From 327423ef670f57a7c75df3964e461835db13a870 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 11:25:37 -0500
Subject: [PATCH] TCB of currently scheduled task on core C is interrupt
 protected on core C. Updated invariants to reflect that.

---
 tasks.c                                          | 16 +++++++---------
 verification/verifast/proof/task_predicates.h    |  4 ++--
 .../verifast/proof/verifast_lock_predicates.h    | 14 ++++++++------
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/tasks.c b/tasks.c
index ea28c42b6..e36ee9ce1 100644
--- a/tasks.c
+++ b/tasks.c
@@ -4134,7 +4134,10 @@ void vTaskSwitchContext( BaseType_t xCoreID )
              interruptState_p(xCoreID, ?state) &*&
              xCoreID == coreID_f() &*&
              interruptsDisabled_f(state) == true &*&
-             coreLocalGlobalVars_p();
+             // opened predicate `coreLocalGlobalVars_p()`
+                pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& 
+                pubTCB_p(gCurrentTCB, 0);
+
 @*/
 //@ ensures true;
 {
@@ -4149,7 +4152,6 @@ void vTaskSwitchContext( BaseType_t xCoreID )
     portGET_TASK_LOCK(); /* Must always acquire the task lock first */
     portGET_ISR_LOCK();
     //@ get_taskISRLockInv();
-    //@ open coreLocalGlobalVars_p();
     {
         /* 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. */
@@ -4164,13 +4166,9 @@ void vTaskSwitchContext( BaseType_t xCoreID )
                 //
                 // TODO: Inspect reason.
                 TaskHandle_t currentHandle = pxCurrentTCB;
-                //@ open taskISRLockInv();
-                //@ assert( foreach(?tasks, _) );
-                //@ foreach_remove(currentHandle, tasks);
-                //@ open absTCB_p(currentHandle);
-                //@ open TCB_p(currentHandle, _);
-                //@ assert( currentHandle->uxCriticalNesting |-> _ );
-                //@ assert( tskTaskControlBlock_uxCriticalNesting(currentHandle, _) );
+                //@ assert( currentHandle == gCurrentTCB );
+                ///@ open taskISRLockInv();
+                //@ open pubTCB_p(gCurrentTCB, 0);
                 UBaseType_t nesting = currentHandle->uxCriticalNesting;
                 configASSERT( nesting == 0 );
             }
diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index cf02d2d5b..f3834bff6 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -104,8 +104,8 @@ predicate absTCB_p(TCB_t* tcb) =
 
 predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack);
 
-predicate pubTCB_p(TCB_t* tcb) =
-    tcb->uxCriticalNesting |-> ?uxCriticalNesting;
+predicate pubTCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) =
+    tcb->uxCriticalNesting |-> uxCriticalNesting;
 @*/
 
 #endif /* TASKS_GH */
\ 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 87bd6d296..512e9df91 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -87,14 +87,16 @@ fixpoint int taskISRLockID_f();
 predicate taskISRLockInv() = 
     integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
     readyLists_p() &*&
+    // Update: The current task on this core is interrupt protected.
+    // TODO: Exclude from `allTasks`.
     // `allTasks` stores pointers to all currently valid tasks (i.e. TCB_t instances)
-    foreach(?tasks, absTCB_p) &*&
+    //foreach(?tasks, absTCB_p) &*&
     // If a task is scheduled, it must be valid
-    [0.5]pointer(&pxCurrentTCBs[coreID_f()], ?scheduledTask) &*&
-    scheduledTask != NULL
-        ? mem(scheduledTask, tasks) == true
-        : true
-    &*&
+    //[0.5]pointer(&pxCurrentTCBs[coreID_f()], ?scheduledTask) &*&
+    //scheduledTask != NULL
+    //    ? mem(scheduledTask, tasks) == true
+    //    : true
+    //&*&
     true;