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 pxPortInitialiseStack for new version of stack predicate.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-02 14:02:42 -04:00
parent f793c96031
commit 249d220ed7
2 changed files with 178 additions and 159 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -60,40 +60,40 @@ typedef intptr_t ptrdiff_t;
typedef intptr_t ssize_t; typedef intptr_t ssize_t;
// # 5 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/malloc.h" 2 // # 5 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/malloc.h" 2
/*@ /*@
// In Standard C, freeing a null pointer is allowed and is a no-op. // In Standard C, freeing a null pointer is allowed and is a no-op.
lemma_auto void malloc_block_null(); lemma_auto void malloc_block_null();
requires emp; requires emp;
ensures malloc_block(0, 0); ensures malloc_block(0, 0);
lemma void malloc_block_limits(void *array); lemma void malloc_block_limits(void *array);
requires [?f]malloc_block(array, ?size); requires [?f]malloc_block(array, ?size);
ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX; ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX;
@*/ @*/
void *malloc(size_t size); void *malloc(size_t size);
//@ requires true; //@ requires true;
/*@ /*@
ensures ensures
result == 0 ? result == 0 ?
emp emp
: :
chars_(result, size, _) &*& malloc_block(result, size) &*& chars_(result, size, _) &*& malloc_block(result, size) &*&
(char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow
@*/ @*/
//@ terminates; //@ terminates;
void *calloc(size_t nmemb, size_t size); void *calloc(size_t nmemb, size_t size);
//@ requires true; //@ requires true;
/*@ /*@
ensures ensures
result == 0 ? result == 0 ?
emp emp
: :
chars(result, nmemb * size, ?cs) &*& malloc_block(result, nmemb * size) &*& all_eq(cs, 0) == true &*& chars(result, nmemb * size, ?cs) &*& malloc_block(result, nmemb * size) &*& all_eq(cs, 0) == true &*&
(char *)0 < result && result + nmemb * size <= (char *)UINTPTR_MAX; // one-past-end does not overflow (char *)0 < result && result + nmemb * size <= (char *)UINTPTR_MAX; // one-past-end does not overflow
@*/ @*/
//@ terminates; //@ terminates;
@ -104,16 +104,16 @@ void free(void *array);
void *realloc(void *array, size_t newSize); void *realloc(void *array, size_t newSize);
//@ requires malloc_block(array, ?size) &*& chars(array, size, ?cs); //@ requires malloc_block(array, ?size) &*& chars(array, size, ?cs);
/*@ /*@
ensures ensures
result == 0 ? result == 0 ?
malloc_block(array, size) &*& chars(array, size, cs) malloc_block(array, size) &*& chars(array, size, cs)
: :
malloc_block(result, newSize) &*& malloc_block(result, newSize) &*&
newSize <= size ? newSize <= size ?
chars(result, _, take(newSize, cs)) chars(result, _, take(newSize, cs))
: :
chars(result, _, cs) &*& chars(result + size, newSize - size, _); chars(result, _, cs) &*& chars(result + size, newSize - size, _);
@*/ @*/
//@ terminates; //@ terminates;
// # 6 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/stdlib.h" 2 // # 6 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/stdlib.h" 2
@ -158,21 +158,21 @@ void memcpy(void *array, void *array0, size_t count);
//@ ensures chars(array, count, cs0) &*& [f]chars(array0, count, cs0); //@ ensures chars(array, count, cs0) &*& [f]chars(array0, count, cs0);
void memmove(void *dest, void *src, size_t count); void memmove(void *dest, void *src, size_t count);
/*@ /*@
requires requires
chars(src, count, ?cs) &*& chars(src, count, ?cs) &*&
dest <= src ? dest <= src ?
chars(dest, src - dest, _) chars(dest, src - dest, _)
: :
chars(src + count, dest - src, _); chars(src + count, dest - src, _);
@*/ @*/
/*@ /*@
ensures ensures
chars(dest, count, cs) &*& chars(dest, count, cs) &*&
dest <= src ? dest <= src ?
chars(dest + count, src - dest, _) chars(dest + count, src - dest, _)
: :
chars(src, dest - src, _); chars(src, dest - src, _);
@*/ @*/
size_t strlen(char *string); size_t strlen(char *string);
@ -193,15 +193,15 @@ char *memchr(char *array, char c, size_t count);
char* strchr(char *str, char c); char* strchr(char *str, char c);
//@ requires [?f]string(str, ?cs); //@ requires [?f]string(str, ?cs);
/*@ ensures /*@ ensures
[f]string(str, cs) &*& [f]string(str, cs) &*&
c == 0 ? c == 0 ?
result == str + length(cs) result == str + length(cs)
: :
result == 0 ? result == 0 ?
mem(c, cs) == false mem(c, cs) == false
: :
mem(c, cs) == true &*& result == str + index_of(c, cs); mem(c, cs) == true &*& result == str + index_of(c, cs);
@*/ @*/
void* memset(void *array, char value, size_t size); void* memset(void *array, char value, size_t size);
@ -548,33 +548,33 @@ typedef void (* TaskFunction_t)( void * );
* must be set in the compiler's include path. */ * must be set in the compiler's include path. */
// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 1 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 1
/* /*
* FreeRTOS SMP Kernel V202110.00 * FreeRTOS SMP Kernel V202110.00
* Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
* Copyright (c) 2021 Raspberry Pi (Trading) Ltd. * Copyright (c) 2021 Raspberry Pi (Trading) Ltd.
* *
* SPDX-License-Identifier: MIT AND BSD-3-Clause * SPDX-License-Identifier: MIT AND BSD-3-Clause
* *
* Permission is hereby granted, free of charge, to any person obtaining a copy of * 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 * this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to * the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of * 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, * the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions: * subject to the following conditions:
* *
* The above copyright notice and this permission notice shall be included in all * The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software. * copies or substantial portions of the Software.
* *
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR * 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 * 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 * 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. * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
* *
* https://www.FreeRTOS.org * https://www.FreeRTOS.org
* https://github.com/FreeRTOS * https://github.com/FreeRTOS
* *
*/ */
// # 37 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" // # 37 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h"
// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/sdks/pico-sdk/src/common/pico_base/include/pico.h" 1 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/sdks/pico-sdk/src/common/pico_base/include/pico.h" 1
@ -4283,14 +4283,14 @@ int spin_lock_claim_unused(bool required);
bool spin_lock_is_claimed(uint lock_num); bool spin_lock_is_claimed(uint lock_num);
// # 39 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 2 // # 39 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 2
/*----------------------------------------------------------- /*-----------------------------------------------------------
* Port specific definitions. * Port specific definitions.
* *
* The settings in this file configure FreeRTOS correctly for the * The settings in this file configure FreeRTOS correctly for the
* given hardware and compiler. * given hardware and compiler.
* *
* These settings should not be altered. * These settings should not be altered.
*----------------------------------------------------------- *-----------------------------------------------------------
*/ */
/* Type definitions. */ /* Type definitions. */
@ -4306,7 +4306,7 @@ bool spin_lock_is_claimed(uint lock_num);
typedef uint32_t TickType_t; typedef uint32_t TickType_t;
/* 32-bit tick type on a 32-bit architecture, so reads of the tick count do /* 32-bit tick type on a 32-bit architecture, so reads of the tick count do
* not need to be guarded with a critical section. */ * not need to be guarded with a critical section. */
@ -4317,13 +4317,13 @@ bool spin_lock_is_claimed(uint lock_num);
/* Reason for rewrite: VeriFast does not support the attriibute `used`. /* Reason for rewrite: VeriFast does not support the attriibute `used`.
*/ */
/* We have to use PICO_DIVIDER_DISABLE_INTERRUPTS as the source of truth rathern than our config, /* We have to use PICO_DIVIDER_DISABLE_INTERRUPTS as the source of truth rathern than our config,
* as our FreeRTOSConfig.h header cannot be included by ASM code - which is what this affects in the SDK */ * as our FreeRTOSConfig.h header cannot be included by ASM code - which is what this affects in the SDK */
@ -4388,11 +4388,11 @@ bool spin_lock_is_claimed(uint lock_num);
/* Note this is a single method with uxAcquire parameter since we have /* Note this is a single method with uxAcquire parameter since we have
* static vars, the method is always called with a compile time constant for * static vars, the method is always called with a compile time constant for
* uxAcquire, and the compiler should dothe right thing! */ * uxAcquire, and the compiler should dothe right thing! */
/* Reason for rewrite: VeriFast does not support local static variables. /* Reason for rewrite: VeriFast does not support local static variables.
*/ */
// # 226 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" // # 226 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h"
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
@ -9975,10 +9975,13 @@ predicate stack_p_2(StackType_t * pxStack,
// Used stack cells // Used stack cells
integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*& integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*&
// Unaligned rest // Unaligned rest
//unalignedRestOfStack_p((char*) pxStack + freeBytes, ulUsedCells, ulUnalignedBytes); //unalignedRestOfStack_p(pxTopOfStack, ulUsedCells, ulUnalignedBytes);
true; true; // skip unaligned part for now
predicate unalignedRestOfStack_p(StackType_t * pxTopOfStack,
uint32_t ulUsedCells,
uint32_t ulUnalignedBytes) =
chars((char*) pxTopOfStack + sizeof(StackType_t) * (ulUsedCells + 1), ulUnalignedBytes, _);
@*/ @*/
/*@ /*@
@ -10417,17 +10420,16 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
ulFreeBytes > 17 * sizeof(StackType_t) &*& ulFreeBytes > 17 * sizeof(StackType_t) &*&
pxStack > 0; pxStack > 0;
@*/ @*/
/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes, /*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack - 16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes);
ulUsedCells, ulUnalignedBytes);
@*/ @*/
{ {
//@ StackType_t* gOldTop = pxTopOfStack; //@ StackType_t* gOldTop = pxTopOfStack;
//@ char* gcStack = (char*) pxStack; //@ char* gcStack = (char*) pxStack;
//@ open stack_p_2(_, _, _, _, _, _); //@ open stack_p_2(_, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) );
//@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) );
// skip stack cell #0 // skip stack cell #0
//@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t)); //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t));
//@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1); //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1);
@ -10435,14 +10437,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
/* Simulate the stack frame as it would be created by a context switch /* Simulate the stack frame as it would be created by a context switch
* interrupt. */ * interrupt. */
pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */ pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) );
// make stack cell #1 available // make stack cell #1 available
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2)); //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2));
//@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1); //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1);
@ -10450,14 +10452,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
*pxTopOfStack = ( 0x01000000 ); /* xPSR */ *pxTopOfStack = ( 0x01000000 ); /* xPSR */
//@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _); //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _);
pxTopOfStack--; pxTopOfStack--;
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) );
// prevent overflow // prevent overflow
//@ ptr_range<void>(pxCode); //@ ptr_range<void>(pxCode);
// make stack cell #2 available // make stack cell #2 available
@ -10467,14 +10469,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
*pxTopOfStack = ( StackType_t ) pxCode; /* PC */ *pxTopOfStack = ( StackType_t ) pxCode; /* PC */
//@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _); //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _);
pxTopOfStack--; pxTopOfStack--;
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) );
// prevent underflow // prevent underflow
//@ ptr_range<void>(prvTaskExitError); //@ ptr_range<void>(prvTaskExitError);
// make stack cell #3 available // make stack cell #3 available
@ -10483,40 +10485,49 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
//@ integers__join(gOldTop-3); //@ integers__join(gOldTop-3);
*pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */ *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */
//@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _); //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _);
pxTopOfStack -= 5; /* R12, R3, R2 and R1. */ pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
// jump to stack cell #7
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 8));
//@ chars_to_integers_(gOldTop-7, sizeof(StackType_t), false, 4);
//@ integers__join(gOldTop-7);
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) );
// prevent overflow // prevent overflow
//@ ptr_range<void>(pvParameters); //@ ptr_range<void>(pvParameters);
// make stack cell #8 available // make stack cell #8 available
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9)); //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9));
//@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 5); //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 1);
//@ integers__join(gOldTop-8); //@ integers__join(gOldTop-8);
*pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */ *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
//@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _); //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _);
// Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack-1, ulFreeBytes - sizeof(StackType_t) * 9, ulUsedCells + 9, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _);
// skip stack cells #9 - #15, leave #16 unused // skip stack cells #9 - #15, leave #16 unused
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 17)); //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 16));
//@ chars_to_integers_(gOldTop-16, sizeof(StackType_t), false, 8); //@ chars_to_integers_(gOldTop-15, sizeof(StackType_t), false, 7);
//@ integers__join(gOldTop-16); //@ integers__join(gOldTop-15);
pxTopOfStack -= 8; /* R11..R4. */ pxTopOfStack -= 8; /* R11..R4. */
// Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes);
//@ assert( stack_p_2(pxStack, ulStackDepth, gOldTop-16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes) );
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) );
//@close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - (sizeof(StackType_t) * 16), ulUsedCells, ulUnalignedBytes);
return pxTopOfStack; return pxTopOfStack;
} }
// # 66 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 66 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2

62
verification/verifast/proof/snippets/rp2040_port_c_snippets.c
View file

@ -117,17 +117,16 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
ulFreeBytes > 17 * sizeof(StackType_t) &*& ulFreeBytes > 17 * sizeof(StackType_t) &*&
pxStack > 0; pxStack > 0;
@*/ @*/
/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes, /*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack - 16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes);
ulUsedCells, ulUnalignedBytes);
@*/ @*/
{ {
//@ StackType_t* gOldTop = pxTopOfStack; //@ StackType_t* gOldTop = pxTopOfStack;
//@ char* gcStack = (char*) pxStack; //@ char* gcStack = (char*) pxStack;
//@ open stack_p_2(_, _, _, _, _, _); //@ open stack_p_2(_, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) );
//@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) );
// skip stack cell #0 // skip stack cell #0
//@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t)); //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t));
//@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1); //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1);
@ -135,14 +134,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
/* Simulate the stack frame as it would be created by a context switch /* Simulate the stack frame as it would be created by a context switch
* interrupt. */ * interrupt. */
pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */ pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) );
// make stack cell #1 available // make stack cell #1 available
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2)); //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2));
//@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1); //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1);
@ -150,14 +149,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
*pxTopOfStack = ( 0x01000000 ); /* xPSR */ *pxTopOfStack = ( 0x01000000 ); /* xPSR */
//@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _); //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _);
pxTopOfStack--; pxTopOfStack--;
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) );
// prevent overflow // prevent overflow
//@ ptr_range<void>(pxCode); //@ ptr_range<void>(pxCode);
// make stack cell #2 available // make stack cell #2 available
@ -167,14 +166,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
*pxTopOfStack = ( StackType_t ) pxCode; /* PC */ *pxTopOfStack = ( StackType_t ) pxCode; /* PC */
//@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _); //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _);
pxTopOfStack--; pxTopOfStack--;
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) );
// prevent underflow // prevent underflow
//@ ptr_range<void>(prvTaskExitError); //@ ptr_range<void>(prvTaskExitError);
// make stack cell #3 available // make stack cell #3 available
@ -183,39 +182,48 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
//@ integers__join(gOldTop-3); //@ integers__join(gOldTop-3);
*pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */ *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */
//@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _); //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _);
pxTopOfStack -= 5; /* R12, R3, R2 and R1. */ pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
// jump to stack cell #7
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 8));
//@ chars_to_integers_(gOldTop-7, sizeof(StackType_t), false, 4);
//@ integers__join(gOldTop-7);
// Ensure maintining stack invariant // Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes); //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _); //@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) );
// prevent overflow // prevent overflow
//@ ptr_range<void>(pvParameters); //@ ptr_range<void>(pvParameters);
// make stack cell #8 available // make stack cell #8 available
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9)); //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9));
//@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 5); //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 1);
//@ integers__join(gOldTop-8); //@ integers__join(gOldTop-8);
*pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */ *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
//@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _); //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _);
// Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack-1, ulFreeBytes - sizeof(StackType_t) * 9, ulUsedCells + 9, ulUnalignedBytes);
//@ open stack_p_2(pxStack, _, _, _, _, _);
// skip stack cells #9 - #15, leave #16 unused // skip stack cells #9 - #15, leave #16 unused
//@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 17)); //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 16));
//@ chars_to_integers_(gOldTop-16, sizeof(StackType_t), false, 8); //@ chars_to_integers_(gOldTop-15, sizeof(StackType_t), false, 7);
//@ integers__join(gOldTop-16); //@ integers__join(gOldTop-15);
pxTopOfStack -= 8; /* R11..R4. */ pxTopOfStack -= 8; /* R11..R4. */
// Ensure maintining stack invariant
//@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes);
//@ assert( stack_p_2(pxStack, ulStackDepth, gOldTop-16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes) );
//@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) ); //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) );
//@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) );
//@close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - (sizeof(StackType_t) * 16), ulUsedCells, ulUnalignedBytes);
return pxTopOfStack; return pxTopOfStack;
} }