Update single core CMBC and unit test (FreeRTOS#1045)

This PR fixes CBMC and unit test for single core FreeRTOS in the FreeRTOS-Kernel PR - FreeRTOS/FreeRTOS-Kernel#716.

- xYieldPendings and xIdleTaskHandles are now an array. Update in FreeRTOS unit test.
-  Update CBMC patches.

Author: chinglee-iot

FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch

@@ -11,40 +11,40 @@ In the case of `uxPendedTicks`, a non-volatile copy of the variable is done
 before the following loop in tasks.c (lines 2231-2255):
 
 {
-	UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */
+       UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */
 
-	if( uxPendedCounts > ( UBaseType_t ) 0U )
-	{
-		do
-		{
-			if( xTaskIncrementTick() != pdFALSE )
-			{
-				xYieldPending = pdTRUE;
-			}
-			else
-			{
-				mtCOVERAGE_TEST_MARKER();
-			}
-			--uxPendedCounts;
-		} while( uxPendedCounts > ( UBaseType_t ) 0U );
+       if( uxPendedCounts > ( UBaseType_t ) 0U )
+       {
+               do
+               {
+                       if( xTaskIncrementTick() != pdFALSE )
+                       {
+                               xYieldPending = pdTRUE;
+                       }
+                       else
+                       {
+                               mtCOVERAGE_TEST_MARKER();
+                       }
+                       --uxPendedCounts;
+               } while( uxPendedCounts > ( UBaseType_t ) 0U );
 
-		uxPendedTicks = 0;
-	}
-	else
-	{
-		mtCOVERAGE_TEST_MARKER();
-	}
+               uxPendedTicks = 0;
+       }
+       else
+       {
+               mtCOVERAGE_TEST_MARKER();
+       }
 }
 
 Here, `uxPendedTicks` could return any value, making it impossible to unwind
 (or unroll) this loop in CBMC.  Therefore, we require `uxPendedTicks` to behave
 as a regular variable so that the loop can be unwound.
 
 diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c
-index 0e7a56c60..b29c19ea5 100644
+index b991b7da4..a220cf0bf 100644
 --- a/FreeRTOS/Source/tasks.c
 +++ b/FreeRTOS/Source/tasks.c
-@@ -339,8 +339,8 @@ portDONT_DISCARD PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL;
+@@ -399,8 +399,8 @@ typedef tskTCB TCB_t;
  PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ]; /**< Prioritised ready tasks. */
  PRIVILEGED_DATA static List_t xDelayedTaskList1;                         /**< Delayed tasks. */
  PRIVILEGED_DATA static List_t xDelayedTaskList2;                         /**< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */
@@ -53,14 +53,14 @@ index 0e7a56c60..b29c19ea5 100644
 +PRIVILEGED_DATA static List_t * pxDelayedTaskList;              /**< Points to the delayed task list currently being used. */
 +PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList;      /**< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
  PRIVILEGED_DATA static List_t xPendingReadyList;                         /**< Tasks that have been readied while the scheduler was suspended.  They will be moved to the ready list when the scheduler is resumed. */
-
+ 
  #if ( INCLUDE_vTaskDelete == 1 )
-@@ -367,7 +367,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType
+@@ -427,7 +427,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType
  PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT;
  PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY;
  PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE;
 -PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U;
 +PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U;
- PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE;
+ PRIVILEGED_DATA static volatile BaseType_t xYieldPendings[ configNUMBER_OF_CORES ] = { pdFALSE };
  PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0;
  PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U;

FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch

@@ -1,20 +1,20 @@
 diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
-index 08d3799da..6681a34f1 100644
+index e87db0f45..1ffbf1191 100644
 --- a/FreeRTOS/Source/queue.c
 +++ b/FreeRTOS/Source/queue.c
-@@ -193,7 +193,7 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION;
+@@ -197,7 +197,7 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION;
   * Copies an item into the queue, either at the front of the queue or the
   * back of the queue.
   */
 -static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
 +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
                                        const void * pvItemToQueue,
                                        const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
-
-@@ -2157,7 +2157,7 @@ void vQueueDelete( QueueHandle_t xQueue )
+ 
+@@ -2263,7 +2263,7 @@ UBaseType_t uxQueueGetQueueItemSize( QueueHandle_t xQueue ) /* PRIVILEGED_FUNCTI
  #endif /* configUSE_MUTEXES */
  /*-----------------------------------------------------------*/
-
+ 
 -static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
 +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
                                        const void * pvItemToQueue,

FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch

@@ -1,17 +1,17 @@
 diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
-index 17a6964e..24a40c29 100644
+index e87db0f45..ec9cc78a9 100644
 --- a/FreeRTOS/Source/queue.c
 +++ b/FreeRTOS/Source/queue.c
-@@ -207,7 +207,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer
- 	 * Checks to see if a queue is a member of a queue set, and if so, notifies
- 	 * the queue set that the queue contains data.
- 	 */
--	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
-+	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
+@@ -213,7 +213,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue,
+  * Checks to see if a queue is a member of a queue set, and if so, notifies
+  * the queue set that the queue contains data.
+  */
+-    static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
++    BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
  #endif
-
+ 
  /*
-@@ -2957,7 +2957,7 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue )
+@@ -3121,7 +3121,7 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue )
 
  #if ( configUSE_QUEUE_SETS == 1 )
 

FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch

@@ -1,22 +1,22 @@
 diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
-index 17a6964e..60ea3e69 100644
+index e87db0f45..98f77012f 100644
 --- a/FreeRTOS/Source/queue.c
 +++ b/FreeRTOS/Source/queue.c
-@@ -175,7 +175,7 @@ typedef xQUEUE Queue_t;
+@@ -177,7 +177,7 @@ typedef xQUEUE Queue_t;
   * to indicate that a task may require unblocking.  When the queue in unlocked
   * these lock counts are inspected, and the appropriate action taken.
   */
 -static void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
 +void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
-
+ 
  /*
   * Uses a critical section to determine if there is any data in a queue.
-@@ -2175,7 +2175,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer
+@@ -2367,7 +2367,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue,
  }
  /*-----------------------------------------------------------*/
-
+ 
 -static void prvUnlockQueue( Queue_t * const pxQueue )
 +void prvUnlockQueue( Queue_t * const pxQueue )
  {
- 	/* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */
-
+     /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */
+ 

FreeRTOS/Test/CBMC/patches/0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patch

@@ -0,0 +1,25 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index e87db0f45..a5f1ac9d0 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -88,12 +88,14 @@ typedef struct SemaphoreData
+ /* If the cooperative scheduler is being used then a yield should not be
+  * performed just because a higher priority task has been woken. */
+     #define queueYIELD_IF_USING_PREEMPTION()
+-#else
+-    #if ( configNUMBER_OF_CORES == 1 )
+-        #define queueYIELD_IF_USING_PREEMPTION()    portYIELD_WITHIN_API()
+-    #else /* #if ( configNUMBER_OF_CORES == 1 ) */
+-        #define queueYIELD_IF_USING_PREEMPTION()    vTaskYieldWithinAPI()
+-    #endif /* #if ( configNUMBER_OF_CORES == 1 ) */
++#endif
++
++#if ( configNUMBER_OF_CORES == 1 ) && ( configUSE_PREEMPTION == 1 )
++    #define queueYIELD_IF_USING_PREEMPTION()    portYIELD_WITHIN_API()
++#endif
++
++#if ( configNUMBER_OF_CORES > 1 ) && ( configUSE_PREEMPTION == 1 )
++    #define queueYIELD_IF_USING_PREEMPTION()    vTaskYieldWithinAPI()
+ #endif
+ 
+ /*

FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/tasks_test_access_functions.h

@@ -1,29 +1,27 @@
 /*
- * FreeRTOS memory safety proofs with CBMC.
- * Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * FreeRTOS V202212.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:
+ * 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 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.
+ * 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://aws.amazon.com/freertos
  * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "cbmc.h"
@@ -77,7 +75,7 @@ void vSetGlobalVariables()
 {
     xPendedTicks = nondet_ubasetype();
     uxSchedulerSuspended = nondet_ubasetype();
-    xYieldPending = nondet_basetype();
+    xYieldPendings[ 0 ] = nondet_basetype();
     xTickCount = nondet_ticktype();
 }
 

FreeRTOS/Test/CMock/tasks/tasks_1_utest.c

@@ -65,11 +65,13 @@ extern volatile TickType_t xTickCount;
 extern volatile UBaseType_t uxTopReadyPriority;
 extern volatile BaseType_t xSchedulerRunning;
 extern volatile TickType_t xPendedTicks;
-extern volatile BaseType_t xYieldPending;
+extern volatile BaseType_t xYieldPendings[];
+#define xYieldPending    xYieldPendings[ 0 ]
 extern volatile BaseType_t xNumOfOverflows;
 extern UBaseType_t uxTaskNumber;
 extern volatile TickType_t xNextTaskUnblockTime;
-extern TaskHandle_t xIdleTaskHandle;
+extern TaskHandle_t xIdleTaskHandles[];
+#define xIdleTaskHandle    xIdleTaskHandles[ 0 ]
 extern volatile UBaseType_t uxSchedulerSuspended;
 
 /* =============================  DEFINES  ================================== */

FreeRTOS/Test/CMock/tasks/tasks_2_utest.c

@@ -64,11 +64,13 @@ extern volatile TickType_t xTickCount;
 extern volatile UBaseType_t uxTopReadyPriority;
 extern volatile BaseType_t xSchedulerRunning;
 extern volatile TickType_t xPendedTicks;
-extern volatile BaseType_t xYieldPending;
+extern volatile BaseType_t xYieldPendings[];
+#define xYieldPending    xYieldPendings[ 0 ]
 extern volatile BaseType_t xNumOfOverflows;
 extern UBaseType_t uxTaskNumber;
 extern volatile TickType_t xNextTaskUnblockTime;
-extern TaskHandle_t xIdleTaskHandle;
+extern TaskHandle_t xIdleTaskHandles[];
+#define xIdleTaskHandle    xIdleTaskHandles[ 0 ]
 extern volatile UBaseType_t uxSchedulerSuspended;