From 7e75d7aa8f3c8b143b2f39dee6c6b41d3ccf9ae9 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Thu, 10 Nov 2022 12:50:48 -0500 Subject: [PATCH] Refined lock predicates and contracts for lock macros to match expected locking discipline. --- tasks.c | 7 +- .../verifast/preprocessed_files/tasks__pp.c | 356 +++++++++++------- .../verifast/proof/nathan/list_predicates.h | 9 +- .../verifast/proof/verifast_lock_predicates.h | 82 +++- .../verifast/proof/verifast_port_contracts.h | 10 +- 5 files changed, 326 insertions(+), 138 deletions(-) diff --git a/tasks.c b/tasks.c index efbe88dee..cafebf385 100644 --- a/tasks.c +++ b/tasks.c @@ -4152,7 +4152,11 @@ BaseType_t xTaskIncrementTick( void ) /*-----------------------------------------------------------*/ void vTaskSwitchContext( BaseType_t xCoreID ) -//@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES; +/*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& + locked(nil) &*& + [?f_ISR]isrLock() &*& + [?f_task]taskLock(); +@*/ //@ ensures true; { /* Acquire both locks: @@ -4165,6 +4169,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) portGET_TASK_LOCK(); /* Must always acquire the task lock first */ portGET_ISR_LOCK(); + //@ get_taskISRLockInv(); { /* vTaskSwitchContext() must never be called from within a critical section. * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */ diff --git a/verification/verifast/preprocessed_files/tasks__pp.c b/verification/verifast/preprocessed_files/tasks__pp.c index b4dca9024..85838c49f 100644 --- a/verification/verifast/preprocessed_files/tasks__pp.c +++ b/verification/verifast/preprocessed_files/tasks__pp.c @@ -67,40 +67,40 @@ typedef intptr_t ptrdiff_t; typedef intptr_t ssize_t; // # 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. -lemma_auto void malloc_block_null(); - requires emp; - ensures malloc_block(0, 0); - -lemma void malloc_block_limits(void *array); - requires [?f]malloc_block(array, ?size); - ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX; - +/*@ + +// In Standard C, freeing a null pointer is allowed and is a no-op. +lemma_auto void malloc_block_null(); + requires emp; + ensures malloc_block(0, 0); + +lemma void malloc_block_limits(void *array); + requires [?f]malloc_block(array, ?size); + ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX; + @*/ void *malloc(size_t size); //@ requires true; - /*@ - ensures - result == 0 ? - emp - : - chars_(result, size, _) &*& malloc_block(result, size) &*& - (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow + /*@ + ensures + result == 0 ? + emp + : + chars_(result, size, _) &*& malloc_block(result, size) &*& + (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow @*/ //@ terminates; void *calloc(size_t nmemb, size_t size); //@ requires true; - /*@ - ensures - result == 0 ? - emp - : - 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 + /*@ + ensures + result == 0 ? + emp + : + 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 @*/ //@ terminates; @@ -111,16 +111,16 @@ void free(void *array); void *realloc(void *array, size_t newSize); //@ requires malloc_block(array, ?size) &*& chars(array, size, ?cs); - /*@ - ensures - result == 0 ? - malloc_block(array, size) &*& chars(array, size, cs) - : - malloc_block(result, newSize) &*& - newSize <= size ? - chars(result, _, take(newSize, cs)) - : - chars(result, _, cs) &*& chars(result + size, newSize - size, _); + /*@ + ensures + result == 0 ? + malloc_block(array, size) &*& chars(array, size, cs) + : + malloc_block(result, newSize) &*& + newSize <= size ? + chars(result, _, take(newSize, cs)) + : + chars(result, _, cs) &*& chars(result + size, newSize - size, _); @*/ //@ terminates; // # 6 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/stdlib.h" 2 @@ -165,21 +165,21 @@ void memcpy(void *array, void *array0, size_t count); //@ ensures chars(array, count, cs0) &*& [f]chars(array0, count, cs0); void memmove(void *dest, void *src, size_t count); - /*@ - requires - chars(src, count, ?cs) &*& - dest <= src ? - chars(dest, src - dest, _) - : - chars(src + count, dest - src, _); + /*@ + requires + chars(src, count, ?cs) &*& + dest <= src ? + chars(dest, src - dest, _) + : + chars(src + count, dest - src, _); @*/ - /*@ - ensures - chars(dest, count, cs) &*& - dest <= src ? - chars(dest + count, src - dest, _) - : - chars(src, dest - src, _); + /*@ + ensures + chars(dest, count, cs) &*& + dest <= src ? + chars(dest + count, src - dest, _) + : + chars(src, dest - src, _); @*/ size_t strlen(char *string); @@ -200,15 +200,15 @@ char *memchr(char *array, char c, size_t count); char* strchr(char *str, char c); //@ requires [?f]string(str, ?cs); - /*@ ensures - [f]string(str, cs) &*& - c == 0 ? - result == str + length(cs) - : - result == 0 ? - mem(c, cs) == false - : - mem(c, cs) == true &*& result == str + index_of(c, cs); + /*@ ensures + [f]string(str, cs) &*& + c == 0 ? + result == str + length(cs) + : + result == 0 ? + mem(c, cs) == false + : + mem(c, cs) == true &*& result == str + index_of(c, cs); @*/ void* memset(void *array, char value, size_t size); @@ -555,33 +555,33 @@ typedef void (* TaskFunction_t)( void * ); * must be set in the compiler's include path. */ // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 1 -/* - * FreeRTOS SMP Kernel V202110.00 - * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. - * Copyright (c) 2021 Raspberry Pi (Trading) Ltd. - * - * SPDX-License-Identifier: MIT AND BSD-3-Clause - * - * 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 - * the Software without restriction, including without limitation the rights to - * 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, - * subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS - * 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 - * 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. - * - * https://www.FreeRTOS.org - * https://github.com/FreeRTOS - * +/* + * FreeRTOS SMP Kernel V202110.00 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * Copyright (c) 2021 Raspberry Pi (Trading) Ltd. + * + * SPDX-License-Identifier: MIT AND BSD-3-Clause + * + * 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 + * the Software without restriction, including without limitation the rights to + * 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, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * 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 + * 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. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + * */ // # 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 @@ -4303,14 +4303,14 @@ int spin_lock_claim_unused(bool required); bool spin_lock_is_claimed(uint lock_num); // # 39 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 2 -/*----------------------------------------------------------- - * Port specific definitions. - * - * The settings in this file configure FreeRTOS correctly for the - * given hardware and compiler. - * - * These settings should not be altered. - *----------------------------------------------------------- +/*----------------------------------------------------------- + * Port specific definitions. + * + * The settings in this file configure FreeRTOS correctly for the + * given hardware and compiler. + * + * These settings should not be altered. + *----------------------------------------------------------- */ /* Type definitions. */ @@ -4326,7 +4326,7 @@ bool spin_lock_is_claimed(uint lock_num); 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. */ @@ -4337,13 +4337,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 */ @@ -4408,11 +4408,11 @@ bool spin_lock_is_claimed(uint lock_num); - /* 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 + /* 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 * 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" /*-----------------------------------------------------------*/ @@ -10077,12 +10077,19 @@ predicate xLIST_ITEM( TickType_t xItemValue, struct xLIST_ITEM *pxNext, struct xLIST_ITEM *pxPrevious, - struct xLIST *pxContainer;) = + struct xLIST *pxContainer;) + = n->xItemValue |-> xItemValue &*& n->pxNext |-> pxNext &*& n->pxPrevious |-> pxPrevious &*& n->pvOwner |-> _ &*& n->pxContainer |-> pxContainer; + +// by Tobias Reinhard +predicate xList_gen(struct xLIST *l) = + l->uxNumberOfItems |-> _ &*& + l->pxIndex |-> _; + @*/ // # 6 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/task_predicates.h" 2 @@ -10389,20 +10396,27 @@ void VF__portRESTORE_INTERRUPTS(uint32_t state); -void VF__portGET_TaskLock(); -//@ requires false; -//@ ensures true; +void VF__portGET_TASK_LOCK(); +//@ requires [?f]taskLock() &*& locked(nil); +//@ ensures taskLockInv() &*& locked( cons( pair(f, taskLockID_f), nil) ); void VF__portGET_ISR_LOCK(); -//@ requires false; -//@ ensures true; +//@ requires [?f]isrLock() &*& locked(?heldLocks); +//@ ensures isrLockInv() &*& locked( cons( pair(f, isrLockID_f), heldLocks) ); // # 72 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/verifast_lock_predicates.h" 1 +/* We follow a minimalistic approach during the definition of the + * lock predicates. So far, the only encapsulate the resources and + * invariants required to verify `vTaskSwitchContext`. + * We are going to extend and refine them when we proceed to verify + * other parts of FRTOS. + */ + /*@ // We assume tha `configNUM_CORES` evaluates to 1. @@ -10454,6 +10468,77 @@ predicate coreLocalLocked(uint32_t coreID); @*/ +/* ---------------------------------------------------------------------- + * Predicates relevant for all locks + */ + +/*@ +predicate locked(list< pair > lockHistory); +@*/ + + + +/* ---------------------------------------------------------------------- + * Task lock and associated global variables from `tasks.c` + */ + +/*@ +fixpoint int taskLockID_f(); + +// Represents an acquired task lock. +predicate taskLock(); + +// Represents an acquired task lock. +// `f` is the fraction held for the unacquired lock. +//predicate taskLocked(real f); + +// Represents the invariant associated with the the task lock, i.e., +// access permissions to the resources protected by the lock. +predicate taskLockInv(); +@*/ + +/* ---------------------------------------------------------------------- + * ISR lock and associated global variables from `tasks.c` + */ + +/*@ +fixpoint int isrLockID_f(); + +// Represents an unacquired ISR lock. +predicate isrLock(); + +// Represents an acquired ISR lock. +// `f` is the fraction held for the unacquired lock. +predicate isrLocked(real f); + +// Represents the invariant associated with the the ISR lock, i.e., +// access permissions to the resources protected by the lock. +predicate isrLockInv() = + foreach(?vfReadyLists, xList_gen); +@*/ + + +/* ---------------------------------------------------------------------- + * Resources protected by both locks. + * Note that the task lock may never be acquired after the ISR lock. + */ + +/*@ +fixpoint int taskISRLockID_f(); + +predicate taskISRLockInv() = + integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _); + + +lemma void get_taskISRLockInv(); +requires locked(?heldLocks) &*& + heldLocks == cons(?i, cons(?t, nil)) &*& + i == pair(?f_isr, isrLockID_f()) &*& + t == pair(?f_task, taskLockID_f()); +ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ); +@*/ + + /* void vf_validate_lock_predicate() @@ -10463,8 +10548,8 @@ void vf_validate_lock_predicate() //@ open_module(); uxCurrentNumberOfTasks = 0; - //@ coreID_f_range(); - //@ close coreLocalGlobalVars(); + ///@ coreID_f_range(); + ///@ close coreLocalGlobalVars(); ///@ close otherGlobalVars(); } */ @@ -13869,7 +13954,11 @@ BaseType_t xTaskIncrementTick( void ) /*-----------------------------------------------------------*/ void vTaskSwitchContext( BaseType_t xCoreID ) -//@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES; +/*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& + locked(nil) &*& + [?f_ISR]isrLock() &*& + [?f_task]taskLock(); +@*/ //@ ensures true; { /* Acquire both locks: @@ -13882,10 +13971,19 @@ void vTaskSwitchContext( BaseType_t xCoreID ) VF__portGET_TASK_LOCK(); /* Must always acquire the task lock first */ VF__portGET_ISR_LOCK(); + //@ get_taskISRLockInv(); { /* vTaskSwitchContext() must never be called from within a critical section. * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */ - assert(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0); + + /* Reason for rewrite: VeriFast cannot handle non-pure assertions. */ + { + UBaseType_t nesting = xTaskGetCurrentTaskHandle()->uxCriticalNesting; + assert(nesting == 0); + } + + + if( uxSchedulerSuspended != ( UBaseType_t ) ( ( char ) 0 ) ) { @@ -13897,7 +13995,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) { xYieldPendings[ xCoreID ] = ( ( char ) 0 ); ; -// # 4212 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4225 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Check for stack overflow, if configured. */ { const uint32_t * pulStack = ( uint32_t * ) xTaskGetCurrentTaskHandle()->pxStack; const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; if( ( pulStack[ 0 ] != ulCheckValue ) || ( pulStack[ 1 ] != ulCheckValue ) || ( pulStack[ 2 ] != ulCheckValue ) || ( pulStack[ 3 ] != ulCheckValue ) ) { vApplicationStackOverflowHook( ( TaskHandle_t ) xTaskGetCurrentTaskHandle(), xTaskGetCurrentTaskHandle()->pcTaskName ); } }; @@ -13914,7 +14012,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) ; /* After the new task is switched in, update the global errno. */ -// # 4246 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4259 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } vPortRecursiveLock(0, spin_lock_instance(14), ( ( char ) 0 )); @@ -14027,7 +14125,7 @@ BaseType_t xTaskRemoveFromEventList( const List_t * pxEventList ) { ( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) ); ; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ; -// # 4372 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4385 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } else { @@ -14067,7 +14165,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem, pxUnblockedTCB = ( ( pxEventListItem )->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too. Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */ assert(pxUnblockedTCB); ( void ) uxListRemove( pxEventListItem ); -// # 4426 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4439 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Remove the task from the delayed list and add it to the ready list. The * scheduler is suspended so interrupts will not be accessing the ready * lists. */ @@ -14240,7 +14338,7 @@ void vTaskMissedYield( void ) for( ; ; ) { -// # 4609 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4622 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* When using preemption tasks of equal priority will be * timesliced. If a task that is sharing the idle priority is ready @@ -14261,7 +14359,7 @@ void vTaskMissedYield( void ) ; } } -// # 4646 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4659 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } @@ -14295,7 +14393,7 @@ static void prvIdleTask( void * pvParameters ) /* See if any tasks have deleted themselves - if so then the idle task * is responsible for freeing the deleted task's TCB and stack. */ prvCheckTasksWaitingTermination(); -// # 4691 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4704 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* When using preemption tasks of equal priority will be * timesliced. If a task that is sharing the idle priority is ready @@ -14316,16 +14414,16 @@ static void prvIdleTask( void * pvParameters ) ; } } -// # 4727 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4740 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* This conditional compilation should use inequality to 0, not equality * to 1. This is to ensure portSUPPRESS_TICKS_AND_SLEEP() is called when * user defined low power mode implementations require * configUSE_TICKLESS_IDLE to be set to a value other than 1. */ -// # 4792 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4805 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } /*-----------------------------------------------------------*/ -// # 4842 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4855 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -14370,7 +14468,7 @@ static void prvIdleTask( void * pvParameters ) /*-----------------------------------------------------------*/ -// # 4902 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4915 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvInitialiseTaskLists( void ) @@ -14472,7 +14570,7 @@ static void prvCheckTasksWaitingTermination( void ) { pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority; } -// # 5014 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5027 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { pxTaskStatus->ulRunTimeCounter = 0; } @@ -14603,7 +14701,7 @@ static void prvCheckTasksWaitingTermination( void ) /*-----------------------------------------------------------*/ -// # 5183 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5196 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -14660,7 +14758,7 @@ static void prvCheckTasksWaitingTermination( void ) free( (void*) pxTCB->pxStack); free( (void*) pxTCB); } -// # 5266 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5279 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } @@ -15165,11 +15263,11 @@ void vTaskYieldWithinAPI( void ) /*-----------------------------------------------------------*/ -// # 5796 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5809 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 5902 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5915 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ -// # 6029 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6042 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ TickType_t uxTaskResetEventItemValue( void ) @@ -15443,7 +15541,7 @@ TickType_t uxTaskResetEventItemValue( void ) /* The task should not have been on an event list. */ assert(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0); -// # 6320 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6333 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { prvYieldForTask( pxTCB, ( ( char ) 0 ) ); } @@ -15737,7 +15835,7 @@ TickType_t uxTaskResetEventItemValue( void ) /*-----------------------------------------------------------*/ -// # 6629 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6642 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, @@ -15813,7 +15911,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, } } } -// # 6741 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6754 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } /* Code below here allows additional code to be inserted into this source file, diff --git a/verification/verifast/proof/nathan/list_predicates.h b/verification/verifast/proof/nathan/list_predicates.h index 7731a0a66..439b092b5 100644 --- a/verification/verifast/proof/nathan/list_predicates.h +++ b/verification/verifast/proof/nathan/list_predicates.h @@ -17,12 +17,19 @@ predicate xLIST_ITEM( TickType_t xItemValue, struct xLIST_ITEM *pxNext, struct xLIST_ITEM *pxPrevious, - struct xLIST *pxContainer;) = + struct xLIST *pxContainer;) + = n->xItemValue |-> xItemValue &*& n->pxNext |-> pxNext &*& n->pxPrevious |-> pxPrevious &*& n->pvOwner |-> _ &*& n->pxContainer |-> pxContainer; + +// by Tobias Reinhard +predicate xList_gen(struct xLIST *l) = + l->uxNumberOfItems |-> _ &*& + l->pxIndex |-> _; + @*/ #endif /* LIST_PREDICATES_H */ \ No newline at end of file diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index ed39a5743..32d8f7390 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -1,6 +1,13 @@ #ifndef VERIFAST_LOCK_PREDICATES_H #define VERIFAST_LOCK_PREDICATES_H +/* We follow a minimalistic approach during the definition of the + * lock predicates. So far, the only encapsulate the resources and + * invariants required to verify `vTaskSwitchContext`. + * We are going to extend and refine them when we proceed to verify + * other parts of FRTOS. + */ + /*@ // We assume tha `configNUM_CORES` evaluates to 1. @@ -52,6 +59,77 @@ predicate coreLocalLocked(uint32_t coreID); @*/ +/* ---------------------------------------------------------------------- + * Predicates relevant for all locks + */ + +/*@ +predicate locked(list< pair > lockHistory); +@*/ + + + +/* ---------------------------------------------------------------------- + * Task lock and associated global variables from `tasks.c` + */ + +/*@ +fixpoint int taskLockID_f(); + +// Represents an acquired task lock. +predicate taskLock(); + +// Represents an acquired task lock. +// `f` is the fraction held for the unacquired lock. +//predicate taskLocked(real f); + +// Represents the invariant associated with the the task lock, i.e., +// access permissions to the resources protected by the lock. +predicate taskLockInv(); +@*/ + +/* ---------------------------------------------------------------------- + * ISR lock and associated global variables from `tasks.c` + */ + +/*@ +fixpoint int isrLockID_f(); + +// Represents an unacquired ISR lock. +predicate isrLock(); + +// Represents an acquired ISR lock. +// `f` is the fraction held for the unacquired lock. +predicate isrLocked(real f); + +// Represents the invariant associated with the the ISR lock, i.e., +// access permissions to the resources protected by the lock. +predicate isrLockInv() = + foreach(?vfReadyLists, xList_gen); +@*/ + + +/* ---------------------------------------------------------------------- + * Resources protected by both locks. + * Note that the task lock may never be acquired after the ISR lock. + */ + +/*@ +fixpoint int taskISRLockID_f(); + +predicate taskISRLockInv() = + integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _); + + +lemma void get_taskISRLockInv(); +requires locked(?heldLocks) &*& + heldLocks == cons(?i, cons(?t, nil)) &*& + i == pair(?f_isr, isrLockID_f()) &*& + t == pair(?f_task, taskLockID_f()); +ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ); +@*/ + + /* void vf_validate_lock_predicate() @@ -61,8 +139,8 @@ void vf_validate_lock_predicate() //@ open_module(); uxCurrentNumberOfTasks = 0; - //@ coreID_f_range(); - //@ close coreLocalGlobalVars(); + ///@ coreID_f_range(); + ///@ close coreLocalGlobalVars(); ///@ close otherGlobalVars(); } */ diff --git a/verification/verifast/proof/verifast_port_contracts.h b/verification/verifast/proof/verifast_port_contracts.h index 5ad986808..2bdb127cf 100644 --- a/verification/verifast/proof/verifast_port_contracts.h +++ b/verification/verifast/proof/verifast_port_contracts.h @@ -46,14 +46,14 @@ void VF__portRESTORE_INTERRUPTS(uint32_t state); #undef portGET_TASK_LOCK #define portGET_TASK_LOCK VF__portGET_TASK_LOCK -void VF__portGET_TaskLock(); -//@ requires false; -//@ ensures true; +void VF__portGET_TASK_LOCK(); +//@ requires [?f]taskLock() &*& locked(nil); +//@ ensures taskLockInv() &*& locked( cons( pair(f, taskLockID_f), nil) ); #undef portGET_ISR_LOCK #define portGET_ISR_LOCK VF__portGET_ISR_LOCK void VF__portGET_ISR_LOCK(); -//@ requires false; -//@ ensures true; +//@ requires [?f]isrLock() &*& locked(?heldLocks); +//@ ensures isrLockInv() &*& locked( cons( pair(f, isrLockID_f), heldLocks) ); #endif /* VERIFAST_PORT_CONTRACTS_H */ \ No newline at end of file