Re: [PATCH v3] docs/misra: add rule 2.1 exceptions

[Julien Grall <julien@xxxxxxx>]

Hi Stefano,

On 09/09/2023 00:03, Stefano Stabellini wrote:
> From: Stefano Stabellini <stefano.stabellini@xxxxxxx>
>
> During the discussions that led to the acceptance of Rule 2.1, we
> decided on a few exceptions that were not properly recorded in
> rules.rst. Add them now.
>
> Signed-off-by: Stefano Stabellini <stefano.stabellini@xxxxxxx>
> Acked-by: Jan Beulich <jbeulich@xxxxxxxx>
> ---
> Nicola, does this work with ECLAIR?
>
> I am referring to the locations of the SAF-2-safe tag on top of
> call_psci_system_off, BUG, etc.
>
> Changes in v3:
> - added SAF-2-safe to safe.json
> - added a few SAF-2-safe examples
> ---
>   docs/misra/rules.rst    | 13 ++++++++++++-
>   docs/misra/safe.json    |  8 ++++++++
>   xen/arch/arm/psci.c     |  1 +
>   xen/arch/x86/shutdown.c |  1 +
>   xen/include/xen/bug.h   |  2 ++
>   5 files changed, 24 insertions(+), 1 deletion(-)
>
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index 34916e266a..82de4c645d 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -107,7 +107,18 @@ maintainers if you want to suggest a change.
>      * - `Rule 2.1 
> <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_01_1.c>`_
>        - Required
>        - A project shall not contain unreachable code
> -     -
> +     - The following are allowed:
> +         - Invariantly constant conditions, e.g. if(IS_ENABLED(CONFIG_HVM)) { 
> S; }
> +         - Switch with a controlling value statically determined not to
> +           match one or more case statements
> +         - Functions that are intended to be referenced only from
> +           assembly code (e.g. 'do_trap_fiq')
> +         - Deliberate unreachability caused by certain macros/functions,
> +           e.g. BUG, assert_failed, panic, etc. See safe.json.
> +         - asm-offsets.c, as they are not linked deliberately, because
> +           they are used to generate definitions for asm modules
> +         - Declarations without initializer are safe, as they are not
> +           executed
>   
>      * - `Rule 2.6 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_06.c>`_
>        - Advisory
> diff --git a/docs/misra/safe.json b/docs/misra/safe.json
> index 39c5c056c7..fc96a99fd5 100644
> --- a/docs/misra/safe.json
> +++ b/docs/misra/safe.json
> @@ -20,6 +20,14 @@
>           },
>           {
>               "id": "SAF-2-safe",
> +            "analyser": {
> +                "eclair": "MC3R1.R2.1"
> +            },
> +            "name": "Rule 2.1: deliberate unreachability",
> +            "text": "Macro or function designed to be unreachable."
> +        },
> +        {
> +            "id": "SAF-3-safe",
>               "analyser": {},
>               "name": "Sentinel",
>               "text": "Next ID to be used"
> diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
> index 695d2fa1f1..2a8527cacc 100644
> --- a/xen/arch/arm/psci.c
> +++ b/xen/arch/arm/psci.c
> @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
>       }
>   }
>   
> +/* SAF-2-safe */
I think any use of SAF-2-safe should be accompanied with an attribute...

>   void call_psci_system_off(void)
... noreturn for function or ...

>   {
>       if ( psci_ver > PSCI_VERSION(0, 1) )
> diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
> index 7619544d14..47e0f59024 100644
> --- a/xen/arch/x86/shutdown.c
> +++ b/xen/arch/x86/shutdown.c
> @@ -118,6 +118,7 @@ static inline void kb_wait(void)
>               break;
>   }
>   
> +/* SAF-2-safe */
>   static void noreturn cf_check __machine_halt(void *unused)
>   {
>       local_irq_disable();
> diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
> index e8a4eea71a..d47c54f034 100644
> --- a/xen/include/xen/bug.h
> +++ b/xen/include/xen/bug.h
> @@ -117,6 +117,7 @@ struct bug_frame {
>   #endif
>   
>   #ifndef BUG
> +/* SAF-2-safe */
>   #define BUG() do {                                              \
>       BUG_FRAME(BUGFRAME_bug,  __LINE__, __FILE__, 0, NULL);      \
>       unreachable();                                              \
... unreachable for macros. But the /* SAF-2-safe */ feels a little bit 
redundant when a function is marked as 'noreturn'.
Is there any way to teach eclair about noreturn?

Cheers,

--
Julien Grall