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

Added proof steps outlining the verification of stack inspection. Also added TODOs concerning rewrites necessary for the verification of the macro.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 16:08:15 -05:00
parent a7d1ca343a
commit 2f0b8bc82f
2 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
include/stack_macros.h
View file

@ -84,6 +84,8 @@
#if ( ( configCHECK_FOR_STACK_OVERFLOW > 1 ) && ( portSTACK_GROWTH < 0 ) ) #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 #ifdef VERIFAST
/* Reason for rewrite: /* Reason for rewrite:
* VeriFast complains about unspecified evaluation order of * VeriFast complains about unspecified evaluation order of

14
tasks.c
View file

@ -4240,8 +4240,18 @@ void vTaskSwitchContext( BaseType_t xCoreID )
/* Check for stack overflow, if configured. */ /* Check for stack overflow, if configured. */
//@ open prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); //@ open prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);
//@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); //@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) );
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(_, _, _, _, _, _);
//@ assert(ulFreeBytes + ulUsedCells >= 3 * sizeof(StackType_t) ); // 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, 3);
// Converting the stack memory into a char squence is allows us to
// verify the inspection of the stack inside this macro.
// However, we the macro contains a call to `vApplicationStackOverflowHook`
// which expects access to the entire TCB. Therefore, we have to close
// the prvTCB_p predicate inside the macro.
// TODO: Convert the macro into a function and push the proof steps
// above into this function.
taskCHECK_FOR_STACK_OVERFLOW(); taskCHECK_FOR_STACK_OVERFLOW();
/* Before the currently running task is switched out, save its errno. */ /* Before the currently running task is switched out, save its errno. */