From 91eb6eefaa0036113ed609ed648bfec59d207880 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Mon, 7 Nov 2022 14:21:42 -0500 Subject: [PATCH] Included reference to core ID in interrupt predicates and added distinction between global and core local variables. --- tasks.c | 10 +- .../verifast/preprocessed_files/tasks__pp.c | 267 ++++++++++-------- .../verifast/proof/verifast_lock_predicates.h | 34 ++- .../verifast/proof/verifast_port_contracts.h | 31 +- 4 files changed, 204 insertions(+), 138 deletions(-) diff --git a/tasks.c b/tasks.c index 0f77349ac..ed3664d57 100644 --- a/tasks.c +++ b/tasks.c @@ -1330,7 +1330,7 @@ static void prvYieldForTask( TCB_t * pxTCB, // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16. chars(pcName, 16, _) &*& *pxCreatedTask |-> _ &*& - interruptState_p(_) &*& + interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); @*/ //@ ensures true; @@ -1876,7 +1876,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, /*-----------------------------------------------------------*/ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) -/*@ requires interruptState_p(_) &*& +/*@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); @*/ /*@ ensures true; @@ -5284,8 +5284,8 @@ static void prvResetNextTaskUnblockTime( void ) #if ( ( INCLUDE_xTaskGetCurrentTaskHandle == 1 ) || ( configUSE_MUTEXES == 1 ) ) TaskHandle_t xTaskGetCurrentTaskHandle( void ) - //@ requires interruptState_p(?irpState); - //@ ensures interruptState_p(irpState) &*& false; + //@ requires interruptState_p(?coreID, ?irpState); + //@ ensures interruptState_p(coreID, irpState) &*& false; { TaskHandle_t xReturn; uint32_t ulState; @@ -5662,7 +5662,7 @@ void vTaskYieldWithinAPI( void ) #if ( portCRITICAL_NESTING_IN_TCB == 1 ) void vTaskEnterCritical( void ) - //@ requires interruptState_p(_) &*& unprotectedGlobalVars(); + //@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); //@ ensures false; { portDISABLE_INTERRUPTS(); diff --git a/verification/verifast/preprocessed_files/tasks__pp.c b/verification/verifast/preprocessed_files/tasks__pp.c index 5ff041e64..dfded4017 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 @@ -4290,14 +4290,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. */ @@ -4313,7 +4313,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. */ @@ -4324,13 +4324,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 */ @@ -4395,11 +4395,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" /*-----------------------------------------------------------*/ @@ -10342,29 +10342,36 @@ bool assert_fct(bool b, const char*) /* FreeRTOS core id is always zero based.*/ static uint VF__get_core_num(void); //@ requires true; -//@ ensures result < configNUM_CORES; +/*@ ensures 0 <= result &*& result < configNUM_CORES &*& + result == coreID_f(); +@*/ +/*@ +// Allow reference to core id in proofs. +fixpoint uint coreID_f(); -/*@ -predicate interruptState_p(uint32_t); - -fixpoint bool interruptsEnabled_f(uint32_t); +lemma void coreID_f_range(); +requires true; +ensures 0 <= coreID_f() &*& coreID_f() < configNUM_CORES; @*/ + + + uint32_t VF__portDISABLE_INTERRUPTS(); -//@ requires interruptState_p(?state); +//@ requires interruptState_p(?coreID, ?state); /*@ ensures result == state &*& - interruptState_p(?newState) &*& - !interruptsEnabled_f(newState); + interruptState_p(coreID, ?newState) &*& + interruptsDisabled_f(newState) == true; @*/ void VF__portRESTORE_INTERRUPTS(uint32_t state); -//@ requires interruptState_p(_); -/*@ ensures interruptState_p(state); +//@ requires interruptState_p(?coreID, _); +/*@ ensures interruptState_p(coreID, state); @*/ @@ -10399,19 +10406,42 @@ predicate otherGlobalVars() = &*& integer_(&xPendedTicks, sizeof(TickType_t), false, _) &*& - integers_(&xYieldPendings, sizeof(BaseType_t), true, 1, _) + integers_(&xYieldPendings, sizeof(BaseType_t), true, configNUM_CORES, _) &*& integer_(&uxTaskNumber, sizeof(UBaseType_t), false, _) &*& integer_(&xNextTaskUnblockTime, sizeof(TickType_t), false, _) &*& - pointers(&xIdleTaskHandle, 1, _); + pointers(&xIdleTaskHandle, configNUM_CORES, _); predicate unprotectedGlobalVars() = [_] integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _); + + @*/ + +/* ---------------------------------------------------------------------- + * Core local variables and access restrictions + */ + +/*@ +predicate interruptState_p(uint32_t coreID, uint32_t state); + +fixpoint bool interruptsDisabled_f(uint32_t); + +predicate coreLocalGlobalVars() = + pointer(&pxCurrentTCBs[coreID_f], _); + +predicate coreLocalLocked(uint32_t coreID); + +//lemma acquireCoreLocalPermissions(); +//requires interruptState_p +@*/ + + + /* void vf_validate_lock_predicate() //@ requires module(tasks__pp, true); @@ -10420,7 +10450,9 @@ void vf_validate_lock_predicate() //@ open_module(); uxCurrentNumberOfTasks = 0; - //@ close tasks_global_vars(); + //@ coreID_f_range(); + //@ close coreLocalGlobalVars(); + ///@ close otherGlobalVars(); } */ // # 73 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 @@ -11546,7 +11578,7 @@ static void prvYieldForTask( TCB_t * pxTCB, // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16. chars(pcName, 16, _) &*& *pxCreatedTask |-> _ &*& - interruptState_p(_) &*& + interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); @*/ //@ ensures true; @@ -11893,7 +11925,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, /*-----------------------------------------------------------*/ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) -/*@ requires interruptState_p(_) &*& +/*@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); @*/ /*@ ensures true; @@ -14593,14 +14625,13 @@ static void prvResetNextTaskUnblockTime( void ) TaskHandle_t xTaskGetCurrentTaskHandle( void ) - //@ requires interruptState_p(?irpState); - //@ ensures interruptState_p(irpState) &*& false; + //@ requires interruptState_p(?coreID, ?irpState); + //@ ensures interruptState_p(coreID, irpState) &*& false; { TaskHandle_t xReturn; uint32_t ulState; ulState = VF__portDISABLE_INTERRUPTS(); - //@ assert( configNUM_CORES == 13 ); xReturn = pxCurrentTCBs[ VF__get_core_num() ]; VF__portRESTORE_INTERRUPTS(ulState); @@ -14972,7 +15003,7 @@ void vTaskYieldWithinAPI( void ) void vTaskEnterCritical( void ) - //@ requires interruptState_p(_) &*& unprotectedGlobalVars(); + //@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); //@ ensures false; { VF__portDISABLE_INTERRUPTS(); diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index 6d1d3b695..ed39a5743 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -17,19 +17,42 @@ predicate otherGlobalVars() = &*& integer_(&xPendedTicks, sizeof(TickType_t), false, _) &*& - integers_(&xYieldPendings, sizeof(BaseType_t), true, 1, _) + integers_(&xYieldPendings, sizeof(BaseType_t), true, configNUM_CORES, _) &*& integer_(&uxTaskNumber, sizeof(UBaseType_t), false, _) &*& integer_(&xNextTaskUnblockTime, sizeof(TickType_t), false, _) &*& - pointers(&xIdleTaskHandle, 1, _); + pointers(&xIdleTaskHandle, configNUM_CORES, _); predicate unprotectedGlobalVars() = [_] integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _); + + @*/ + +/* ---------------------------------------------------------------------- + * Core local variables and access restrictions + */ + +/*@ +predicate interruptState_p(uint32_t coreID, uint32_t state); + +fixpoint bool interruptsDisabled_f(uint32_t); + +predicate coreLocalGlobalVars() = + pointer(&pxCurrentTCBs[coreID_f], _); + +predicate coreLocalLocked(uint32_t coreID); + +//lemma acquireCoreLocalPermissions(); +//requires interruptState_p +@*/ + + + /* void vf_validate_lock_predicate() //@ requires module(tasks__pp, true); @@ -38,8 +61,13 @@ void vf_validate_lock_predicate() //@ open_module(); uxCurrentNumberOfTasks = 0; - //@ close tasks_global_vars(); + //@ coreID_f_range(); + //@ close coreLocalGlobalVars(); + ///@ close otherGlobalVars(); } */ + + + #endif /* VERIFAST_LOCK_PREDICATES_H */ \ No newline at end of file diff --git a/verification/verifast/proof/verifast_port_contracts.h b/verification/verifast/proof/verifast_port_contracts.h index 82171e9ec..5ad986808 100644 --- a/verification/verifast/proof/verifast_port_contracts.h +++ b/verification/verifast/proof/verifast_port_contracts.h @@ -12,29 +12,36 @@ /* FreeRTOS core id is always zero based.*/ static uint VF__get_core_num(void); //@ requires true; -//@ ensures result < configNUM_CORES; - - -/*@ -predicate interruptState_p(uint32_t); - -fixpoint bool interruptsEnabled_f(uint32_t); +/*@ ensures 0 <= result &*& result < configNUM_CORES &*& + result == coreID_f(); @*/ +/*@ +// Allow reference to core id in proofs. +fixpoint uint coreID_f(); + +lemma void coreID_f_range(); +requires true; +ensures 0 <= coreID_f() &*& coreID_f() < configNUM_CORES; +@*/ + + + + #undef portDISABLE_INTERRUPTS #define portDISABLE_INTERRUPTS VF__portDISABLE_INTERRUPTS uint32_t VF__portDISABLE_INTERRUPTS(); -//@ requires interruptState_p(?state); +//@ requires interruptState_p(?coreID, ?state); /*@ ensures result == state &*& - interruptState_p(?newState) &*& - !interruptsEnabled_f(newState); + interruptState_p(coreID, ?newState) &*& + interruptsDisabled_f(newState) == true; @*/ #undef portRESTORE_INTERRUPTS #define portRESTORE_INTERRUPTS(ulState) VF__portRESTORE_INTERRUPTS(ulState) void VF__portRESTORE_INTERRUPTS(uint32_t state); -//@ requires interruptState_p(_); -/*@ ensures interruptState_p(state); +//@ requires interruptState_p(?coreID, _); +/*@ ensures interruptState_p(coreID, state); @*/ #undef portGET_TASK_LOCK