Added info about available tasks to lock predicate.

tasks.c

@@ -30,6 +30,7 @@
      */
 
     //@ #include <bitops.gh>
+    //@ #include "list.gh"
 
     /* The following includes will be visible to VeriFast in the preprocessed
      * code. VeriFast requires includes to occur befor definitions. Hence,
@@ -37,6 +38,8 @@
      * ones. 
      */
     //VF_include #include "FreeRTOSConfig.h"
+
+    //VF_macro #define NULL 0
 #endif /* VERIFAST */
 
 
@@ -64,6 +67,7 @@
     #include "verifast_proof_defs.h"
     #include "stack_predicates.h"
     #include "task_predicates.h"
+    #include "ready_list_predicates.h"
     #include "verifast_RP2040_axioms.h"
     #include "verifast_prelude_extended.h"
     #include "verifast_bitops_extended.h"
@@ -4160,8 +4164,15 @@ void vTaskSwitchContext( BaseType_t xCoreID )
                 // "This potentially side-effecting expression is not supported in this position, because of C's unspecified evaluation order"
                 //
                 // TODO: Inspect reason.
-                TaskHandle_t handle = pxCurrentTCB;
-                UBaseType_t nesting = handle->uxCriticalNesting;
+                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, _) );
+                UBaseType_t nesting = currentHandle->uxCriticalNesting;
                 configASSERT( nesting == 0 );
             }
         #else

verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh

@@ -49,6 +49,7 @@ rewrite "const [*]" "*"
 
 echo "Uncomment special includes to allow VeriFast proofs to refer to config macros"
 rewrite "//VF_include #include" "#include"
+rewrite "//VF_macro #" "#"
 
 #echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
 #echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"

verification/verifast/proof/ready_list_predicates.h

@@ -0,0 +1,8 @@
+#ifndef READY_LIST_PREDICATES_H
+#define READY_LIST_PREDICATES_H
+
+/*@
+predicate readyLists_p();
+@*/
+
+#endif /* READY_LIST_PREDICATES_H */

verification/verifast/proof/task_predicates.h

@@ -72,7 +72,7 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
     // Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16.
     chars_(tcb->pcTaskName, 16, _) &*&
 
-    tcb->uxCriticalNesting |-> _ &*&
+    tcb->uxCriticalNesting |-> ?uxCriticalNesting &*&
     tcb->uxTCBNumber |-> _ &*&
     tcb->uxTaskNumber |-> _ &*&
     tcb->uxBasePriority |-> _ &*&
@@ -87,6 +87,10 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
     uchars((unsigned char*) tcb->ucNotifyState, 1, _) &*&
 
     tcb->ucDelayAborted |-> _;
+
+
+predicate absTCB_p(TCB_t* tcb) =
+    TCB_p(tcb, _);
 @*/
 
 #endif /* TASKS_GH */

verification/verifast/proof/verifast_lock_predicates.h

@@ -1,6 +1,15 @@
 #ifndef VERIFAST_LOCK_PREDICATES_H
 #define VERIFAST_LOCK_PREDICATES_H
 
+
+
+//
+/*@
+// Declare predicate defined in "task_predicates.h"
+// Why does including that header not solve them problem?
+//predicate absTCB_p(TCB_t* tcb);
+@*/
+
 /* 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`.
@@ -118,7 +127,17 @@ predicate isrLockInv() =
 fixpoint int taskISRLockID_f();
 
 predicate taskISRLockInv() = 
-    integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _);
+    integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
+    readyLists_p() &*&
+    // `allTasks` stores pointers to all currently valid tasks (i.e. TCB_t instances)
+    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
+    &*&
+    true;
 
 
 lemma void get_taskISRLockInv();