Update Cellular_CommonInit error handling (#163)

* Update Cellular_CommonInit error handling * Update size table * Update CBMC for Cellular_CommonInit
FreeRTOS · Jan 31, 2024 · df553bd · df553bd
1 parent f1097fb
commit df553bd
Show file tree

Hide file tree

Showing 6 changed files with 307 additions and 46 deletions.
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
@@ -25,7 +25,7 @@
     <tr>
         <td>cellular_common_api.c</td>
         <td><center>0.7K</center></td>
-        <td><center>0.6K</center></td>
+        <td><center>0.7K</center></td>
     </tr>
     <tr>
         <td>cellular_common.c</td>
@@ -45,6 +45,6 @@
     <tr>
         <td><b>Total estimates</b></td>
         <td><b><center>15.1K</center></b></td>
-        <td><b><center>13.6K</center></b></td>
+        <td><b><center>13.7K</center></b></td>
     </tr>
 </table>
diff --git a/source/cellular_common_api.c b/source/cellular_common_api.c
@@ -146,25 +146,58 @@ CellularError_t Cellular_CommonInit( CellularHandle_t * pCellularHandle,
     CellularError_t cellularStatus = CELLULAR_SUCCESS;
     CellularContext_t * pContext = NULL;
 
-    /* Init the common library. */
-    cellularStatus = _Cellular_LibInit( pCellularHandle, pCommInterface, pTokenTable );
-
-    /* Init the module. */
-    if( cellularStatus == CELLULAR_SUCCESS )
+    if( pCellularHandle == NULL )
     {
-        pContext = *pCellularHandle;
-        cellularStatus = Cellular_ModuleInit( pContext, &pContext->pModuleContext );
+        LogError( ( "Cellular_CommonInit pCellularHandle is NULL." ) );
+        cellularStatus = CELLULAR_INVALID_HANDLE;
     }
-
-    /* Setup UE, URC and query register status. */
-    if( cellularStatus == CELLULAR_SUCCESS )
+    else if( pCommInterface == NULL )
     {
-        cellularStatus = Cellular_ModuleEnableUE( pContext );
+        LogError( ( "Cellular_CommonInit pCommInterface is NULL." ) );
+        cellularStatus = CELLULAR_BAD_PARAMETER;
     }
-
-    if( cellularStatus == CELLULAR_SUCCESS )
+    else if( pTokenTable == NULL )
+    {
+        LogError( ( "Cellular_CommonInit pTokenTable is NULL." ) );
+        cellularStatus = CELLULAR_BAD_PARAMETER;
+    }
+    else
     {
-        cellularStatus = Cellular_ModuleEnableUrc( pContext );
+        /* Init the common library. */
+        cellularStatus = _Cellular_LibInit( pCellularHandle, pCommInterface, pTokenTable );
+
+        if( cellularStatus == CELLULAR_SUCCESS )
+        {
+            pContext = ( CellularContext_t * ) ( *pCellularHandle );
+
+            cellularStatus = Cellular_ModuleInit( pContext, &pContext->pModuleContext );
+
+            if( cellularStatus == CELLULAR_SUCCESS )
+            {
+                cellularStatus = Cellular_ModuleEnableUE( pContext );
+
+                if( cellularStatus == CELLULAR_SUCCESS )
+                {
+                    cellularStatus = Cellular_ModuleEnableUrc( pContext );
+                }
+
+                if( cellularStatus != CELLULAR_SUCCESS )
+                {
+                    /* Clean up the resource allocated by cellular module here if
+                     * Cellular_ModuleEnableUE or Cellular_ModuleEnableUrc returns
+                     * error. */
+                    ( void ) Cellular_ModuleCleanUp( pContext );
+                }
+            }
+
+            if( cellularStatus != CELLULAR_SUCCESS )
+            {
+                /* Clean up the resource in cellular common library if any of the
+                 * module port function returns error. Error returned by _Cellular_LibInit
+                 * is already handled in the implementation. */
+                ( void ) _Cellular_LibCleanup( pContext );
+            }
+        }
     }
 
     return cellularStatus;

diff --git a/test/cbmc/proofs/Cellular_CommonInit/Cellular_CommonInit_harness.c b/test/cbmc/proofs/Cellular_CommonInit/Cellular_CommonInit_harness.c
@@ -96,5 +96,7 @@ void harness()
     * Initialize the member of Cellular_CommonInit.
     ****************************************************************/
 
-    Cellular_CommonInit( nondet_bool() ? NULL : &pHandle, &CellularCommInterface, &tokenTable );
+    Cellular_CommonInit( nondet_bool() ? NULL : &pHandle,
+                         nondet_bool() ? NULL : &CellularCommInterface,
+                         nondet_bool() ? NULL : &tokenTable );
 }
diff --git a/test/cbmc/proofs/Cellular_CommonInit/Makefile b/test/cbmc/proofs/Cellular_CommonInit/Makefile
@@ -24,7 +24,7 @@ HARNESS_ENTRY=harness
 HARNESS_FILE=Cellular_CommonInit_harness
 PROOF_UID = Cellular_CommonInit
 
-DEFINES +=
+DEFINES += -DCBMC_TEST_CELLULAR_MODULE_RETURN_ERROR=1
 INCLUDES +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
@@ -35,4 +35,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
 
+UNWINDSET += __CPROVER_file_local_cellular_common_c_libClose.0:20
+
 include ../Makefile.common
diff --git a/test/cbmc/sources/cellular_modules.c b/test/cbmc/sources/cellular_modules.c
@@ -33,41 +33,64 @@
 /* Include paths for public enums, structures, and macros. */
 #include "cellular_common_portable.h"
 
-CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext,
-                                     void ** ppModuleContext )
-{
-    CellularError_t ret = nondet_int();
+#if ( CBMC_TEST_CELLULAR_MODULE_RETURN_ERROR == 1 )
 
-    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
-    return ret;
-}
+    CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext,
+                                         void ** ppModuleContext )
+    {
+        CellularError_t ret = nondet_int();
 
+        __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+        return ret;
+    }
 
-CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext )
-{
-    CellularError_t ret = nondet_int();
+    CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext )
+    {
+        CellularError_t ret = nondet_int();
 
-    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
-    return ret;
-}
+        __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+        return ret;
+    }
 
+    CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
+    {
+        CellularError_t ret = nondet_int();
 
-CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
-{
-    CellularError_t ret = nondet_int();
+        __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+        return ret;
+    }
 
-    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
-    return ret;
-}
+    CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext )
+    {
+        CellularError_t ret = nondet_int();
 
+        __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+        return ret;
+    }
 
-CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext )
-{
-    CellularError_t ret = nondet_int();
+#else /* #if ( CBMC_TEST_CELLULAR_MODULE_NO_ERROR == 1 ) */
 
-    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
-    return ret;
-}
+    CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext,
+                                         void ** ppModuleContext )
+    {
+        return CELLULAR_SUCCESS;
+    }
 
+    CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext )
+    {
+        return CELLULAR_SUCCESS;
+    }
+
+    CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
+    {
+        return CELLULAR_SUCCESS;
+    }
+
+    CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext )
+    {
+        return CELLULAR_SUCCESS;
+    }
+
+#endif /* #if ( CBMC_TEST_CELLULAR_MODULE_NO_ERROR == 1 ) */
 
 /* ========================================================================== */