From 4eb2fa573e352565ea6819bc23931d449a7c52c8 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 14:18:03 -0500
Subject: [PATCH] Wrote contracts for lock release operations.

---
 tasks.c                                         |  4 +++-
 .../verifast/proof/verifast_lock_predicates.h   |  8 +++++++-
 .../verifast/proof/verifast_port_contracts.h    | 17 +++++++++++++++--
 3 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/tasks.c b/tasks.c
index 4f0f498c2..abf0b1670 100644
--- a/tasks.c
+++ b/tasks.c
@@ -4152,7 +4152,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
 
     portGET_TASK_LOCK(); /* Must always acquire the task lock first */
     portGET_ISR_LOCK();
-    //@ get_taskISRLockInv();
+    //@ produce_taskISRLockInv();
     {
         /* 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. */
@@ -4253,6 +4253,8 @@ void vTaskSwitchContext( BaseType_t xCoreID )
             #endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */
         }
     }
+    //@ close taskISRLockInv();
+    //@ consume_taskISRLockInv();
     portRELEASE_ISR_LOCK();
     portRELEASE_TASK_LOCK();
 }
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index 4a0324bec..948b4d93d 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -103,13 +103,19 @@ predicate taskISRLockInv() =
     true;
 
 
-lemma void get_taskISRLockInv();
+lemma void produce_taskISRLockInv();
 requires locked(?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();
+
+
+lemma void consume_taskISRLockInv();
+requires locked( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*&
+         taskISRLockInv();
+ensures  locked(otherLocks);
 @*/
 
 
diff --git a/verification/verifast/proof/verifast_port_contracts.h b/verification/verifast/proof/verifast_port_contracts.h
index b2c9b145a..c2af62d39 100644
--- a/verification/verifast/proof/verifast_port_contracts.h
+++ b/verification/verifast/proof/verifast_port_contracts.h
@@ -53,12 +53,25 @@ void VF__portRESTORE_INTERRUPTS(uint32_t ulState);
 #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) );
+//@ ensures taskLockInv() &*& locked( 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);
 
 #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) );
+//@ ensures isrLockInv() &*& locked( 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);
+
 
 #endif /* VERIFAST_PORT_CONTRACTS_H */
\ No newline at end of file