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

Axiomatized knowledge about RP2040 architecture and added tmp workaround for over/underflows.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-25 14:34:01 -04:00
parent 06bc0fbb2d
commit 8b958c7834
3 changed files with 302 additions and 243 deletions
Download patch file Download diff file Expand all files Collapse all files

12
tasks.c
View file

@ -28,6 +28,7 @@
#ifdef VERIFAST
#include "verifast_proof_defs.h"
#include "task_predicates.h"
#include "verifast_RP2040_axioms.h"
#endif
/* Standard includes. */
@ -1481,6 +1482,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
#if ( portSTACK_GROWTH < 0 )
{
pxTopOfStack = &( pxNewTCB->pxStack[ ulStackDepth - ( uint32_t ) 1 ] );
// Axiomatize that pointers on RP2040 are 32bit
//@ uint32_t_ptr_range(pxTopOfStack);
// TODO: How can we prove this?
// Assume that no underflow occurs
//@ assume( 0 <= (( (uint32_t) pxTopOfStack) & ~(7)) );
// TODO: How can we prove this?
// Assume that now 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(). */
/* Check the alignment of the calculated top of stack is correct. */

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

File diff suppressed because it is too large Load diff

19
verification/verifast/proof_setup/verifast_RP2040_axioms.h Normal file
View file

@ -0,0 +1,19 @@
#ifndef VERIFAST_RP2040_AXIOMS_H
#define VERIFAST_RP2040_AXIOMS_H
#include "stdint.h"
/*
* The lemmas in this file axiomatize that the RP2040 architecture uses
* 32bit pointers.
*/
/*@
// Axiomatizes that: 0 <= ptr <= 2^32 - 1
lemma void uint32_t_ptr_range(uint32_t* ptr);
requires true;
ensures 0 <= (int) ptr &*& (int) ptr <= 4294967295;
@*/
#endif