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

Verified alignment check of stack top pointer.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-28 13:59:45 -04:00
parent eedbfe3255
commit ead381f413
4 changed files with 273 additions and 249 deletions
Download patch file Download diff file Expand all files Collapse all files

28
tasks.c
View file

@ -59,6 +59,7 @@
#include "task_predicates.h" #include "task_predicates.h"
#include "verifast_RP2040_axioms.h" #include "verifast_RP2040_axioms.h"
#include "verifast_prelude_extended.h" #include "verifast_prelude_extended.h"
#include "verifast_bitops_extended.h"
#include "verifast_asm.h" #include "verifast_asm.h"
#include "snippets/rp2040_port_c_snippets.c" #include "snippets/rp2040_port_c_snippets.c"
@ -1507,10 +1508,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
// Axiomatize that pointers on RP2040 are 32bit // Axiomatize that pointers on RP2040 are 32bit
//@ ptr_range<uint32_t>(pxTopOfStack); //@ ptr_range<uint32_t>(pxTopOfStack);
// TODO: How can we prove this?
// Assume that no underflow occurs
///@ assume( 0 <= (( (uint32_t) pxTopOfStack) & ~(7)) );
/* Convert top and mask to VeriFast bitvectors and establish /* Convert top and mask to VeriFast bitvectors and establish
* relation to C variables. * relation to C variables.
* Note that on RP2040: * Note that on RP2040:
@ -1523,21 +1520,22 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
//@ bitnot_def(gMask, gzMask); //@ bitnot_def(gMask, gzMask);
//@ bitand_def((int) pxTopOfStack, gzTop, ~gMask, Z_not(gzMask)); //@ bitand_def((int) pxTopOfStack, gzTop, ~gMask, Z_not(gzMask));
// TODO: How can we prove this?
// Assume that no overflow occurs.
///@ assume( (((uint32_t) pxTopOfStack) & ~7) <= UINTPTR_MAX);
pxTopOfStack = ( StackType_t * ) ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack ) & ( ~( ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) ) ); /*lint !e923 !e9033 !e9078 MISRA exception. Avoiding casts between pointers and integers is not practical. Size differences accounted for using portPOINTER_SIZE_TYPE type. Checked by assert(). */ pxTopOfStack = ( StackType_t * ) ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack ) & ( ~( ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) ) ); /*lint !e923 !e9033 !e9078 MISRA exception. Avoiding casts between pointers and integers is not practical. Size differences accounted for using portPOINTER_SIZE_TYPE type. Checked by assert(). */
//@ assert( pxTopOfStack <= gOldTop );
//@ assert( gOldTop - 7 <= pxTopOfStack ); // The following alignment assertions hold but take very long to verify.
//@ assert(false); ///@ assert( pxTopOfStack <= gOldTop );
///@ assert( gOldTop - 7 <= pxTopOfStack );
/* Check the alignment of the calculated top of stack is correct. */ /* Check the alignment of the calculated top of stack is correct. */
#ifndef VERIFAST
// TODO: Figure out how to handle configASSERT/__builtin_expect // Same as above but for aligned top pointer:
// maybe replace by VF assertion. //@ Z gzAlignedTop = Z_of_uint32((int) pxTopOfStack);
configASSERT( ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack & ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) == 0UL ) ); //@ bitand_def((int) pxTopOfStack, gzAlignedTop, gMask, gzMask);
#endif /* VERIFAST */
configASSERT( ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack & ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) == 0UL ) );
//@ assert(false);
#if ( configRECORD_STACK_HIGH_ADDRESS == 1 ) #if ( configRECORD_STACK_HIGH_ADDRESS == 1 )
{ {

480
verification/verifast/preprocessed_files/tasks--pp.c
View file

File diff suppressed because it is too large Load diff

10
verification/verifast/proof/verifast_bitops_extended.h Normal file
View file

@ -0,0 +1,10 @@
#ifndef VERIFAST_BITOPS_EXTENDED_H
#define VERIFAST_BITOPS_EXTENDED_H
/*@
lemma void bitand_idempotent_right(int l, int r);
requires true;
ensures (l & r) == ((l & r) & r);
@*/
#endif /* VERIFAST_BITOPS_EXTENDED_H */

4
verification/verifast/proof_setup/verifast_proof_defs.h
View file

@ -20,4 +20,8 @@
#define pdTRUE ( ( char ) 1 ) #define pdTRUE ( ( char ) 1 )
#define pd_U_FALSE ( ( unsigned char ) pdFALSE ) #define pd_U_FALSE ( ( unsigned char ) pdFALSE )
#define pd_U_TRUE ( ( unsigned char ) pdTRUE ) #define pd_U_TRUE ( ( unsigned char ) pdTRUE )
#undef assert
#undef configASSERT
#define configASSERT(x) assert(x)
#endif /* VERIFAST_DEFS_H */ #endif /* VERIFAST_DEFS_H */