diff --git a/tasks.c b/tasks.c index 95d771983..c31607902 100644 --- a/tasks.c +++ b/tasks.c @@ -902,9 +902,9 @@ static void prvYieldForTask( TCB_t * pxTCB, // interrupts are disabled and locks acquired interruptState_p(xCoreID, ?state) &*& interruptsDisabled_f(state) == true &*& - taskLockInv() &*& - isrLockInv() &*& - taskISRLockInv() + taskLockInv_p() &*& + isrLockInv_p() &*& + taskISRLockInv_p() &*& // opened predicate `coreLocalInterruptInv_p()` pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& @@ -919,9 +919,9 @@ static void prvYieldForTask( TCB_t * pxTCB, // interrupts are disabled and locks acquired interruptState_p(xCoreID, state) &*& interruptsDisabled_f(state) == true &*& - taskLockInv() &*& - isrLockInv() &*& - taskISRLockInv() + taskLockInv_p() &*& + isrLockInv_p() &*& + taskISRLockInv_p() &*& // opened predicate `coreLocalInterruptInv_p()` pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& @@ -932,7 +932,7 @@ static void prvYieldForTask( TCB_t * pxTCB, prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ { - //@ open taskISRLockInv(); + //@ open taskISRLockInv_p(); //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) ); //@ assert( gTopReadyPriority == uxTopReadyPriority); UBaseType_t uxCurrentPriority = uxTopReadyPriority; @@ -945,7 +945,7 @@ static void prvYieldForTask( TCB_t * pxTCB, #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) BaseType_t xPriorityDropped = pdFALSE; #endif - //@ close taskISRLockInv(); + //@ close taskISRLockInv_p(); while( xTaskScheduled == pdFALSE ) /*@ invariant @@ -955,9 +955,9 @@ static void prvYieldForTask( TCB_t * pxTCB, // interrupts are disabled and locks acquired interruptState_p(xCoreID, state) &*& interruptsDisabled_f(state) == true &*& - taskLockInv() &*& - isrLockInv() &*& - taskISRLockInv() + taskLockInv_p() &*& + isrLockInv_p() &*& + taskISRLockInv_p() &*& // opened predicate `coreLocalInterruptInv_p()` pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& @@ -986,7 +986,7 @@ static void prvYieldForTask( TCB_t * pxTCB, } #endif - //@ open taskISRLockInv(); + //@ open taskISRLockInv_p(); //@ open readyLists_p(?gCellLists); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_split(pxReadyTasksLists, uxCurrentPriority); @@ -4281,9 +4281,9 @@ void vTaskSwitchContext( BaseType_t xCoreID ) xCoreID == coreID_f() &*& // access to locks and disabled interrupts - locked(nil) &*& - [?f_ISR]isrLock() &*& - [?f_task]taskLock() &*& + locked_p(nil) &*& + [?f_ISR]isrLock_p() &*& + [?f_task]taskLock_p() &*& interruptState_p(xCoreID, ?state) &*& interruptsDisabled_f(state) == true &*& @@ -4297,9 +4297,9 @@ void vTaskSwitchContext( BaseType_t xCoreID ) @*/ /*@ ensures // all locks are released and interrupts remain disabled - locked(nil) &*& - [f_ISR]isrLock() &*& - [f_task]taskLock() &*& + locked_p(nil) &*& + [f_ISR]isrLock_p() &*& + [f_task]taskLock_p() &*& interruptState_p(xCoreID, state) &*& // opened predicate `coreLocalInterruptInv_p()` @@ -4347,13 +4347,13 @@ void vTaskSwitchContext( BaseType_t xCoreID ) configASSERT( pxCurrentTCB->uxCriticalNesting == 0 ); #endif /* VERIFAST */ - //@ open taskISRLockInv(); + //@ open taskISRLockInv_p(); if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE ) { /* The scheduler is currently suspended - do not allow a context * switch. */ xYieldPendings[ xCoreID ] = pdTRUE; - //@ close taskISRLockInv(); + //@ close taskISRLockInv_p(); } else { @@ -4400,7 +4400,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) /* Select a new task to run using either the generic C or port * optimised asm code. */ - //@ close taskISRLockInv(); + //@ close taskISRLockInv_p(); ( void ) prvSelectHighestPriorityTask( xCoreID ); traceTASK_SWITCHED_IN(); diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index 0bcc05bd3..640a4e07f 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -32,9 +32,6 @@ predicate coreLocalInterruptInv_p() = //pubTCB_p(currentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& coreLocalSeg_TCB_p(currentTCB, ?gCriticalNesting); - - -predicate coreLocalLocked(uint32_t coreID); @*/ @@ -43,7 +40,7 @@ predicate coreLocalLocked(uint32_t coreID); */ /*@ -predicate locked(list< pair > lockHistory); +predicate locked_p(list< pair > lockHistory); @*/ @@ -56,11 +53,11 @@ predicate locked(list< pair > lockHistory); fixpoint int taskLockID_f(); // Represents an acquired task lock. -predicate taskLock(); +predicate taskLock_p(); // Represents the invariant associated with the the task lock, i.e., // access permissions to the resources protected by the lock. -predicate taskLockInv(); +predicate taskLockInv_p(); @*/ /* ---------------------------------------------------------------------- @@ -71,11 +68,11 @@ predicate taskLockInv(); fixpoint int isrLockID_f(); // Represents an unacquired ISR lock. -predicate isrLock(); +predicate isrLock_p(); // Represents the invariant associated with the the ISR lock, i.e., // access permissions to the resources protected by the lock. -predicate isrLockInv(); +predicate isrLockInv_p(); @*/ @@ -87,7 +84,7 @@ predicate isrLockInv(); /*@ fixpoint int taskISRLockID_f(); -predicate taskISRLockInv() = +predicate taskISRLockInv_p() = integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _) &*& @@ -101,18 +98,18 @@ predicate taskISRLockInv() = lemma void produce_taskISRLockInv(); -requires locked(?heldLocks) &*& +requires locked_p(?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) ) &*& - taskISRLockInv(); +ensures locked_p( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*& + taskISRLockInv_p(); lemma void consume_taskISRLockInv(); -requires locked( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*& - taskISRLockInv(); -ensures locked(otherLocks); +requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*& + taskISRLockInv_p(); +ensures locked_p(otherLocks); @*/ diff --git a/verification/verifast/proof/verifast_port_contracts.h b/verification/verifast/proof/verifast_port_contracts.h index 77c645b96..620e82b75 100644 --- a/verification/verifast/proof/verifast_port_contracts.h +++ b/verification/verifast/proof/verifast_port_contracts.h @@ -54,26 +54,26 @@ void VF__portRESTORE_INTERRUPTS(uint32_t ulState); #undef portGET_TASK_LOCK #define portGET_TASK_LOCK VF__portGET_TASK_LOCK void VF__portGET_TASK_LOCK(); -//@ requires [?f]taskLock() &*& locked(nil); -//@ ensures taskLockInv() &*& locked( cons( pair(f, taskLockID_f()), nil) ); +//@ requires [?f]taskLock_p() &*& locked_p(nil); +//@ ensures taskLockInv_p() &*& locked_p( cons( pair(f, taskLockID_f()), nil) ); #undef portRELEASE_TASK_LOCK #define portRELEASE_TASK_LOCK VF__portRELEASE_TASK_LOCK void VF__portRELEASE_TASK_LOCK(); -//@ requires taskLockInv() &*& locked( cons( pair(?f, taskLockID_f()), nil) ); -//@ ensures [f]taskLock() &*& locked(nil); +//@ requires taskLockInv_p() &*& locked_p( cons( pair(?f, taskLockID_f()), nil) ); +//@ ensures [f]taskLock_p() &*& locked_p(nil); #undef portGET_ISR_LOCK #define portGET_ISR_LOCK VF__portGET_ISR_LOCK void VF__portGET_ISR_LOCK(); -//@ requires [?f]isrLock() &*& locked(?heldLocks); -//@ ensures isrLockInv() &*& locked( cons( pair(f, isrLockID_f()), heldLocks) ); +//@ requires [?f]isrLock_p() &*& locked_p(?heldLocks); +//@ ensures isrLockInv_p() &*& locked_p( cons( pair(f, isrLockID_f()), heldLocks) ); #undef portRELEASE_ISR_LOCK #define portRELEASE_ISR_LOCK VF__portRELEASE_ISR_LOCK void VF__portRELEASE_ISR_LOCK(); -//@ requires isrLockInv() &*& locked( cons( pair(?f, isrLockID_f()), ?heldLocks) ); -//@ ensures [f]isrLock() &*& locked(heldLocks); +//@ requires isrLockInv_p() &*& locked_p( cons( pair(?f, isrLockID_f()), ?heldLocks) ); +//@ ensures [f]isrLock_p() &*& locked_p(heldLocks); #endif /* VERIFAST_PORT_CONTRACTS_H */ \ No newline at end of file