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

Renamed predicates to comply with naming conventions

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-29 09:47:50 -05:00
parent 014acb9a00
commit e8b8234416
3 changed files with 41 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

42
tasks.c
View file

@ -902,9 +902,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
// interrupts are disabled and locks acquired // interrupts are disabled and locks acquired
interruptState_p(xCoreID, ?state) &*& interruptState_p(xCoreID, ?state) &*&
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true &*&
taskLockInv() &*& taskLockInv_p() &*&
isrLockInv() &*& isrLockInv_p() &*&
taskISRLockInv() taskISRLockInv_p()
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
@ -919,9 +919,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
// interrupts are disabled and locks acquired // interrupts are disabled and locks acquired
interruptState_p(xCoreID, state) &*& interruptState_p(xCoreID, state) &*&
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true &*&
taskLockInv() &*& taskLockInv_p() &*&
isrLockInv() &*& isrLockInv_p() &*&
taskISRLockInv() taskISRLockInv_p()
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*&
@ -932,7 +932,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack);
@*/ @*/
{ {
//@ open taskISRLockInv(); //@ open taskISRLockInv_p();
//@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) ); //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) );
//@ assert( gTopReadyPriority == uxTopReadyPriority); //@ assert( gTopReadyPriority == uxTopReadyPriority);
UBaseType_t uxCurrentPriority = uxTopReadyPriority; UBaseType_t uxCurrentPriority = uxTopReadyPriority;
@ -945,7 +945,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
#if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
BaseType_t xPriorityDropped = pdFALSE; BaseType_t xPriorityDropped = pdFALSE;
#endif #endif
//@ close taskISRLockInv(); //@ close taskISRLockInv_p();
while( xTaskScheduled == pdFALSE ) while( xTaskScheduled == pdFALSE )
/*@ invariant /*@ invariant
@ -955,9 +955,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
// interrupts are disabled and locks acquired // interrupts are disabled and locks acquired
interruptState_p(xCoreID, state) &*& interruptState_p(xCoreID, state) &*&
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true &*&
taskLockInv() &*& taskLockInv_p() &*&
isrLockInv() &*& isrLockInv_p() &*&
taskISRLockInv() taskISRLockInv_p()
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*&
@ -986,7 +986,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
} }
#endif #endif
//@ open taskISRLockInv(); //@ open taskISRLockInv_p();
//@ open readyLists_p(?gCellLists); //@ open readyLists_p(?gCellLists);
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
//@ List_array_split(pxReadyTasksLists, uxCurrentPriority); //@ List_array_split(pxReadyTasksLists, uxCurrentPriority);
@ -4281,9 +4281,9 @@ void vTaskSwitchContext( BaseType_t xCoreID )
xCoreID == coreID_f() xCoreID == coreID_f()
&*& &*&
// access to locks and disabled interrupts // access to locks and disabled interrupts
locked(nil) &*& locked_p(nil) &*&
[?f_ISR]isrLock() &*& [?f_ISR]isrLock_p() &*&
[?f_task]taskLock() &*& [?f_task]taskLock_p() &*&
interruptState_p(xCoreID, ?state) &*& interruptState_p(xCoreID, ?state) &*&
interruptsDisabled_f(state) == true interruptsDisabled_f(state) == true
&*& &*&
@ -4297,9 +4297,9 @@ void vTaskSwitchContext( BaseType_t xCoreID )
@*/ @*/
/*@ ensures // all locks are released and interrupts remain disabled /*@ ensures // all locks are released and interrupts remain disabled
locked(nil) &*& locked_p(nil) &*&
[f_ISR]isrLock() &*& [f_ISR]isrLock_p() &*&
[f_task]taskLock() &*& [f_task]taskLock_p() &*&
interruptState_p(xCoreID, state) interruptState_p(xCoreID, state)
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
@ -4347,13 +4347,13 @@ void vTaskSwitchContext( BaseType_t xCoreID )
configASSERT( pxCurrentTCB->uxCriticalNesting == 0 ); configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );
#endif /* VERIFAST */ #endif /* VERIFAST */
//@ open taskISRLockInv(); //@ open taskISRLockInv_p();
if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE ) if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE )
{ {
/* The scheduler is currently suspended - do not allow a context /* The scheduler is currently suspended - do not allow a context
* switch. */ * switch. */
xYieldPendings[ xCoreID ] = pdTRUE; xYieldPendings[ xCoreID ] = pdTRUE;
//@ close taskISRLockInv(); //@ close taskISRLockInv_p();
} }
else else
{ {
@ -4400,7 +4400,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
/* Select a new task to run using either the generic C or port /* Select a new task to run using either the generic C or port
* optimised asm code. */ * optimised asm code. */
//@ close taskISRLockInv(); //@ close taskISRLockInv_p();
( void ) prvSelectHighestPriorityTask( xCoreID ); ( void ) prvSelectHighestPriorityTask( xCoreID );
traceTASK_SWITCHED_IN(); traceTASK_SWITCHED_IN();

27
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -32,9 +32,6 @@ predicate coreLocalInterruptInv_p() =
//pubTCB_p(currentTCB, 0) &*& //pubTCB_p(currentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
coreLocalSeg_TCB_p(currentTCB, ?gCriticalNesting); coreLocalSeg_TCB_p(currentTCB, ?gCriticalNesting);
predicate coreLocalLocked(uint32_t coreID);
@*/ @*/
@ -43,7 +40,7 @@ predicate coreLocalLocked(uint32_t coreID);
*/ */
/*@ /*@
predicate locked(list< pair<real, int> > lockHistory); predicate locked_p(list< pair<real, int> > lockHistory);
@*/ @*/
@ -56,11 +53,11 @@ predicate locked(list< pair<real, int> > lockHistory);
fixpoint int taskLockID_f(); fixpoint int taskLockID_f();
// Represents an acquired task lock. // Represents an acquired task lock.
predicate taskLock(); predicate taskLock_p();
// Represents the invariant associated with the the task lock, i.e., // Represents the invariant associated with the the task lock, i.e.,
// access permissions to the resources protected by the lock. // access permissions to the resources protected by the lock.
predicate taskLockInv(); predicate taskLockInv_p();
@*/ @*/
/* ---------------------------------------------------------------------- /* ----------------------------------------------------------------------
@ -71,11 +68,11 @@ predicate taskLockInv();
fixpoint int isrLockID_f(); fixpoint int isrLockID_f();
// Represents an unacquired ISR lock. // Represents an unacquired ISR lock.
predicate isrLock(); predicate isrLock_p();
// Represents the invariant associated with the the ISR lock, i.e., // Represents the invariant associated with the the ISR lock, i.e.,
// access permissions to the resources protected by the lock. // access permissions to the resources protected by the lock.
predicate isrLockInv(); predicate isrLockInv_p();
@*/ @*/
@ -87,7 +84,7 @@ predicate isrLockInv();
/*@ /*@
fixpoint int taskISRLockID_f(); fixpoint int taskISRLockID_f();
predicate taskISRLockInv() = predicate taskISRLockInv_p() =
integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _) integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _)
&*& &*&
@ -101,18 +98,18 @@ predicate taskISRLockInv() =
lemma void produce_taskISRLockInv(); lemma void produce_taskISRLockInv();
requires locked(?heldLocks) &*& requires locked_p(?heldLocks) &*&
heldLocks == cons(?i, cons(?t, nil)) &*& heldLocks == cons(?i, cons(?t, nil)) &*&
i == pair(?f_isr, isrLockID_f()) &*& i == pair(?f_isr, isrLockID_f()) &*&
t == pair(?f_task, taskLockID_f()); t == pair(?f_task, taskLockID_f());
ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*& ensures locked_p( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*&
taskISRLockInv(); taskISRLockInv_p();
lemma void consume_taskISRLockInv(); lemma void consume_taskISRLockInv();
requires locked( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*& requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*&
taskISRLockInv(); taskISRLockInv_p();
ensures locked(otherLocks); ensures locked_p(otherLocks);
@*/ @*/

16
verification/verifast/proof/verifast_port_contracts.h
View file

@ -54,26 +54,26 @@ void VF__portRESTORE_INTERRUPTS(uint32_t ulState);
#undef portGET_TASK_LOCK #undef portGET_TASK_LOCK
#define portGET_TASK_LOCK VF__portGET_TASK_LOCK #define portGET_TASK_LOCK VF__portGET_TASK_LOCK
void VF__portGET_TASK_LOCK(); void VF__portGET_TASK_LOCK();
//@ requires [?f]taskLock() &*& locked(nil); //@ requires [?f]taskLock_p() &*& locked_p(nil);
//@ ensures taskLockInv() &*& locked( cons( pair(f, taskLockID_f()), nil) ); //@ ensures taskLockInv_p() &*& locked_p( cons( pair(f, taskLockID_f()), nil) );
#undef portRELEASE_TASK_LOCK #undef portRELEASE_TASK_LOCK
#define portRELEASE_TASK_LOCK VF__portRELEASE_TASK_LOCK #define portRELEASE_TASK_LOCK VF__portRELEASE_TASK_LOCK
void VF__portRELEASE_TASK_LOCK(); void VF__portRELEASE_TASK_LOCK();
//@ requires taskLockInv() &*& locked( cons( pair(?f, taskLockID_f()), nil) ); //@ requires taskLockInv_p() &*& locked_p( cons( pair(?f, taskLockID_f()), nil) );
//@ ensures [f]taskLock() &*& locked(nil); //@ ensures [f]taskLock_p() &*& locked_p(nil);
#undef portGET_ISR_LOCK #undef portGET_ISR_LOCK
#define portGET_ISR_LOCK VF__portGET_ISR_LOCK #define portGET_ISR_LOCK VF__portGET_ISR_LOCK
void VF__portGET_ISR_LOCK(); void VF__portGET_ISR_LOCK();
//@ requires [?f]isrLock() &*& locked(?heldLocks); //@ requires [?f]isrLock_p() &*& locked_p(?heldLocks);
//@ ensures isrLockInv() &*& locked( cons( pair(f, isrLockID_f()), heldLocks) ); //@ ensures isrLockInv_p() &*& locked_p( cons( pair(f, isrLockID_f()), heldLocks) );
#undef portRELEASE_ISR_LOCK #undef portRELEASE_ISR_LOCK
#define portRELEASE_ISR_LOCK VF__portRELEASE_ISR_LOCK #define portRELEASE_ISR_LOCK VF__portRELEASE_ISR_LOCK
void VF__portRELEASE_ISR_LOCK(); void VF__portRELEASE_ISR_LOCK();
//@ requires isrLockInv() &*& locked( cons( pair(?f, isrLockID_f()), ?heldLocks) ); //@ requires isrLockInv_p() &*& locked_p( cons( pair(?f, isrLockID_f()), ?heldLocks) );
//@ ensures [f]isrLock() &*& locked(heldLocks); //@ ensures [f]isrLock_p() &*& locked_p(heldLocks);
#endif /* VERIFAST_PORT_CONTRACTS_H */ #endif /* VERIFAST_PORT_CONTRACTS_H */