From 7adb08eff5ec3cd229a778cbba570590ff426fba Mon Sep 17 00:00:00 2001 From: chinglee-iot <61685396+chinglee-iot@users.noreply.github.com> Date: Mon, 24 Jul 2023 18:12:20 +0800 Subject: [PATCH] Update single core CMBC and unit test (#1045) This PR fixes CBMC and unit test for single core FreeRTOS in the FreeRTOS-Kernel PR - https://github.com/FreeRTOS/FreeRTOS-Kernel/pull/716. - xYieldPendings and xIdleTaskHandles are now an array. Update in FreeRTOS unit test. - Update CBMC patches. --- ...atile-qualifier-from-tasks-variables.patch | 52 +++++++++---------- ...emove-static-from-prvCopyDataToQueue.patch | 10 ++-- ...atic-from-prvNotifyQueueSetContainer.patch | 18 +++---- ...07-Remove-static-from-prvUnlockQueue.patch | 14 ++--- ...acro-for-queueYIELD_IF_USING_PREEMPT.patch | 25 +++++++++ .../tasks_test_access_functions.h | 40 +++++++------- FreeRTOS/Test/CMock/tasks/tasks_1_utest.c | 6 ++- FreeRTOS/Test/CMock/tasks/tasks_2_utest.c | 6 ++- 8 files changed, 99 insertions(+), 72 deletions(-) create mode 100644 FreeRTOS/Test/CBMC/patches/0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patch diff --git a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch index 847bc56732..d4bd80f0be 100644 --- a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch +++ b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -11,29 +11,29 @@ 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 @@ -41,10 +41,10 @@ Here, `uxPendedTicks` could return any value, making it impossible to unwind 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; diff --git a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch index 6414bdf2d1..a6bf80196e 100644 --- a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch +++ b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -1,8 +1,8 @@ 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. */ @@ -10,11 +10,11 @@ index 08d3799da..6681a34f1 100644 +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, diff --git a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch index bb8e724d74..65d46dc21c 100644 --- a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch +++ b/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 ) diff --git a/FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch b/FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch index eaae401c60..ccb6c6e4fa 100644 --- a/FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch +++ b/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. */ + diff --git a/FreeRTOS/Test/CBMC/patches/0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patch b/FreeRTOS/Test/CBMC/patches/0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patch new file mode 100644 index 0000000000..57da0dfb9d --- /dev/null +++ b/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 + + /* diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/tasks_test_access_functions.h b/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/tasks_test_access_functions.h index be3085c3ee..b1cf88e56a 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/tasks_test_access_functions.h +++ b/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(); } diff --git a/FreeRTOS/Test/CMock/tasks/tasks_1_utest.c b/FreeRTOS/Test/CMock/tasks/tasks_1_utest.c index 559858e0ed..b9ba3b1e1d 100644 --- a/FreeRTOS/Test/CMock/tasks/tasks_1_utest.c +++ b/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 ================================== */ diff --git a/FreeRTOS/Test/CMock/tasks/tasks_2_utest.c b/FreeRTOS/Test/CMock/tasks/tasks_2_utest.c index 3d24565a5c..929108a776 100644 --- a/FreeRTOS/Test/CMock/tasks/tasks_2_utest.c +++ b/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;