Clear timers in shutdown and suspend (#413)

Co-authored-by: Bujain <bujain@amazon.com>
aws · Jan 14, 2022 · ab4d425 · ab4d425
1 parent 7a43c34
commit ab4d425
Show file tree

Hide file tree

Showing 8 changed files with 72 additions and 4 deletions.
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
@@ -9,8 +9,8 @@
     </tr>
     <tr>
         <td>ota.c</td>
-        <td><center>8.0K</center></td>
-        <td><center>7.2K</center></td>
+        <td><center>8.1K</center></td>
+        <td><center>7.3K</center></td>
     </tr>
     <tr>
         <td>ota_interface.c</td>
@@ -39,7 +39,7 @@
     </tr>
     <tr>
         <td><b>Total estimates</b></td>
-        <td><b><center>12.1K</center></b></td>
-        <td><b><center>11.0K</center></b></td>
+        <td><b><center>12.2K</center></b></td>
+        <td><b><center>11.1K</center></b></td>
     </tr>
 </table>
diff --git a/source/ota.c b/source/ota.c
@@ -3186,6 +3186,14 @@ OtaState_t OTA_Shutdown( uint32_t ticksToWait,
     {
         otaAgent.unsubscribeOnShutdown = unsubscribeFlag;
 
+        /* Stop and delete the request timer. */
+        ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaRequestTimer );
+        ( void ) otaAgent.pOtaInterface->os.timer.delete( OtaRequestTimer );
+
+        /* Stop and delete the self-test timer. */
+        ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaSelfTestTimer );
+        ( void ) otaAgent.pOtaInterface->os.timer.delete( OtaSelfTestTimer );
+
         /*
          * Send shutdown signal to OTA Agent task.
          */
@@ -3386,6 +3394,9 @@ OtaErr_t OTA_Suspend( void )
         /* Stop the request timer. */
         ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaRequestTimer );
 
+        /* Stop the self-test timer. */
+        ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaSelfTestTimer );
+
         /*
          * Send event to OTA agent task.
          */
@@ -3416,6 +3427,19 @@ OtaErr_t OTA_Resume( void )
     /* Check if OTA Agent is running. */
     if( otaAgent.state != OtaAgentStateStopped )
     {
+        /*
+         * Resume timers.
+         */
+        ( void ) otaAgent.pOtaInterface->os.timer.start( OtaSelfTestTimer,
+                                                         "OtaSelfTestTimer",
+                                                         otaconfigSELF_TEST_RESPONSE_WAIT_MS,
+                                                         otaTimerCallback );
+
+        ( void ) otaAgent.pOtaInterface->os.timer.start( OtaRequestTimer,
+                                                         "OtaRequestTimer",
+                                                         otaconfigFILE_REQUEST_WAIT_MS,
+                                                         otaTimerCallback );
+
         /*
          * Send event to OTA agent task.
          */

diff --git a/test/cbmc/include/stubs.h b/test/cbmc/include/stubs.h
@@ -109,3 +109,6 @@ OtaPalStatus_t createFilePalStub( OtaFileContext_t * const pFileContext );
 
 /* Stub to request a fileblock from the Data plane. */
 OtaErr_t requestFileBlockStub( OtaAgentContext_t * pAgentCtx );
+
+/* Stub to delete timer. */
+OtaOsStatus_t deleteTimerStub( OtaTimerId_t otaTimerId );
diff --git a/test/cbmc/proofs/OTA_Resume/Makefile b/test/cbmc/proofs/OTA_Resume/Makefile
@@ -8,14 +8,20 @@ PROOF_UID = OTA_Resume_harness
 
 INCLUDES += -I$(SRCDIR)/source/dependency/coreJSON/source/include/
 INCLUDES += -I$(SRCDIR)/source/
+INCLUDES += -I$(SRCDIR)/test/cbmc/include/
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/source/ota.c
 
+DEFINES += -Dstatic=""
+
 NONDET_STATIC += "--nondet-static"
 
 REMOVE_FUNCTION_BODY += OTA_SignalEvent
 
+RESTRICT_FUNCTION_POINTER += OTA_Resume.function_pointer_call.1/startTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Resume.function_pointer_call.2/startTimerStub
+
 # If this proof is found to consume huge amounts of RAM, you can set the
 # EXPENSIVE variable. With new enough versions of the proof tools, this will
 # restrict the number of EXPENSIVE CBMC jobs running at once. See the

diff --git a/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c b/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c
@@ -26,6 +26,9 @@
  */
 /*  Ota Agent includes. */
 #include "ota.h"
+#include "stubs.h"
+
+extern OtaAgentContext_t otaAgent;
 
 bool OTA_SignalEvent( const OtaEventMsg_t * const pEventMsg )
 {
@@ -36,5 +39,11 @@ bool OTA_SignalEvent( const OtaEventMsg_t * const pEventMsg )
 
 void OTA_Resume_harness()
 {
+    OtaInterfaces_t otaInterface;
+
+    /* Initialize os timers. */
+    otaInterface.os.timer.start = startTimerStub;
+    otaAgent.pOtaInterface = &otaInterface;
+
     OTA_Resume();
 }
diff --git a/test/cbmc/proofs/OTA_Shutdown/Makefile b/test/cbmc/proofs/OTA_Shutdown/Makefile
@@ -18,6 +18,11 @@ PROJECT_SOURCES += $(SRCDIR)/source/ota.c
 
 REMOVE_FUNCTION_BODY += OTA_SignalEvent
 
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.1/stopTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.2/deleteTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.3/stopTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.4/deleteTimerStub
+
 # If this proof is found to consume huge amounts of RAM, you can set the
 # EXPENSIVE variable. With new enough versions of the proof tools, this will
 # restrict the number of EXPENSIVE CBMC jobs running at once. See the

diff --git a/test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c b/test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c
@@ -26,6 +26,7 @@
  */
 /*  Ota Agent includes. */
 #include "ota.h"
+#include "stubs.h"
 
 extern OtaAgentContext_t otaAgent;
 
@@ -34,9 +35,16 @@ void OTA_Shutdown_harness()
     OtaState_t state;
     uint32_t ticksToWait;
     uint8_t unsubscribeFlag;
+    OtaInterfaces_t otaInterface;
 
     otaAgent.state = state;
 
+    /* Initialize os timers functions. */
+    otaInterface.os.timer.stop = stopTimerStub;
+    otaInterface.os.timer.delete = deleteTimerStub;
+
+    otaAgent.pOtaInterface = &otaInterface;
+
     /* This assumption is required to have an upper bound on the unwinding of while loop in
      * OTA_Shutdown. This does not model the exact behavior of the code since the limitation of CBMC
      * is that it checks concurrent code in sequential manner.*/

diff --git a/test/cbmc/source/stubs.c b/test/cbmc/source/stubs.c
@@ -304,3 +304,16 @@ OtaErr_t requestFileBlockStub( OtaAgentContext_t * pAgentCtx )
 
     return err;
 }
+
+OtaOsStatus_t deleteTimerStub( OtaTimerId_t otaTimerId )
+{
+    OtaOsStatus_t status;
+
+    /* status must have values only from the OtaOsStatus_t enum. */
+    __CPROVER_assume( ( status >= OtaOsSuccess ) && ( status <= OtaOsTimerDeleteFailed ) );
+
+    __CPROVER_assert( ( otaTimerId == OtaSelfTestTimer ) || ( otaTimerId == OtaRequestTimer ),
+                      "Error: Expected otaTimerId to be either OtaSelfTestTimer or OtaRequestTimer." );
+
+    return status;
+}