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

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

On Mon, 11 Sep 2023, Julien Grall wrote:
> 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?

Actually I had the same thought while writing this patch. If we can
adopt unreachable and noreturn consistently maybe we don't need
SAF-2-safe. If the checker can support it.

Nicola, what do you think?