len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 14:15:12 -05:00
Code Issues Projects Releases Packages Wiki Activity

Verified macro taskCHECK_FOR_STACK_OVERFLOW.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-17 09:20:21 -05:00
parent 2f0b8bc82f
commit d3bda01f16
5 changed files with 81 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

48
include/stack_macros.h
View file

@ -93,21 +93,67 @@
* - `vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName );`
*
*/
#define taskCHECK_FOR_STACK_OVERFLOW() \
#define taskCHECK_FOR_STACK_OVERFLOW() VF__taskCHECK_FOR_STACK_OVERFLOW()
void VF__taskCHECK_FOR_STACK_OVERFLOW()
/*@ requires prvTCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*&
pubTCB_p(gCurrentTCB, ?uxCriticalNesting) &*&
// chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
interruptState_p(coreID_f(), ?state) &*&
interruptsDisabled_f(state) == true &*&
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB);
@*/
/*@ ensures prvTCB_p(gCurrentTCB, ulFreeBytesOnStack) &*&
pubTCB_p(gCurrentTCB, uxCriticalNesting) &*&
// chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
interruptState_p(coreID_f(), state) &*&
interruptsDisabled_f(state) == true &*&
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); \
@*/ \
{ \
/*@ open prvTCB_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 prvTCB_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 prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); \
} \
@*/ \
}
#else
#define taskCHECK_FOR_STACK_OVERFLOW() \

6
include/task.h
View file

@ -1863,6 +1863,12 @@ configSTACK_DEPTH_TYPE uxTaskGetStackHighWaterMark2( TaskHandle_t xTask ) PRIVIL
*/
void vApplicationStackOverflowHook( TaskHandle_t xTask,
char * pcTaskName );
/*@ requires prvTCB_p(xTask, ?ulFreeBytesOnStack) &*&
pubTCB_p(xTask, ?uxCriticalNesting);
@*/
/*@ ensures prvTCB_p(xTask, ulFreeBytesOnStack) &*&
pubTCB_p(xTask, uxCriticalNesting);
@*/
#endif

23
tasks.c
View file

@ -56,7 +56,16 @@
#include "FreeRTOS.h"
#include "task.h"
#include "timers.h"
#include "stack_macros.h"
#ifndef VERIFAST
/* Reason for rewrite:
* The stack macros rely on macros defined later in this file, e.g.,
* `pxCurrentTCB`. We need to delay this inclusion until the task macros
* have been defined. Otherwise, VeriFast will report unknown symbols when
* checking the stack macro proofs.
*/
#include "stack_macros.h"
#endif /* VERIFAST */
/* Verifast proof setup
*
@ -381,6 +390,18 @@ PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Poi
PRIVILEGED_DATA static List_t * volatile 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. */
#ifdef VERIFAST
/* Reason for rewrite:
* The stack macros rely on some of the macros defined above, e.g.,
* `pxCurrentTCB`. We need to delay this inclusion until the relevant task
* macros have been defined. Otherwise, VeriFast will report unknown symbols
* when checking the stack macro proofs.
*/
#include "stack_macros.h"
#endif /* VERIFAST */
#if ( INCLUDE_vTaskDelete == 1 )
PRIVILEGED_DATA static List_t xTasksWaitingTermination; /*< Tasks that have been deleted - but their memory not yet freed. */

2
verification/verifast/proof/stack_predicates.h
View file

@ -28,7 +28,7 @@ predicate stack_p_2(StackType_t * pxStack,
// `taskCHECK_FOR_STACK_OVERFLOW` macro on RP2040 port expects minimal stack size
ulFreeBytes >= 0 &*&
ulUsedCells >= 0 &*&
ulFreeBytes + ulUsedCells * sizeof(StackType_t) >= 3 * sizeof(StackType_t);
ulFreeBytes + ulUsedCells * sizeof(StackType_t) >= 4 * sizeof(StackType_t);
predicate unalignedRestOfStack_p(char* p, uint32_t ulUnalignedBytes) =
chars(p, ulUnalignedBytes, _);

2
verification/verifast/start-vfide--preprocessed.sh
View file

@ -13,7 +13,7 @@ PP_SCRIPT_DIR="$START_WD/custom_build_scripts_RP2040"
PP_SCRIPT="./preprocess_tasks_c.sh"
PP_TASK_C="$START_WD/preprocessed_files/tasks__pp.c"
FONT_SIZE=16
FONT_SIZE=17
# Flags to SKIP expensive proofs:
# - VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT