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

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

> > > 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?
A couple of remarks:
- if you put the noreturn attribute on some functions, then surely the 
code after those is
reported as unreachable. ECLAIR should pick up all forms of noreturn 
automatically; otherwise, a simple configuration can be used.
- Note that the cause of unreachability in the vast majority of cases is 
the call to
__builtin_unreachable(), therefore a textual deviation on the definition 
of unreachable, plus
a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF 
comment is not
sufficient, since deviations comments are meant to be applied at the top 
expansion location,
which is not on the macro definition).
This is what it should look like, roughly:

-config=MC3R1.R2.1,reports+={deliberate, 
"any_area(any_loc(text(^<REGEX>$, -1)))"}
#if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
/* SAF-2-safe */
#define unreachable() do {} while (1)
#else
/* SAF-2-safe */
#define unreachable() __builtin_unreachable()
#endif

where REGEX will match the translation of SAF-2-safe.

However, this will then entail that *some* SAF comments are treated 
specially and, moreover,
that some modification to the definition of unreachable won't work
(e.g.
#define M() __builtin_unreachable()
/* SAF-2-safe */
#define unreachable() M()

My opinion is that it's far easier for this to be an eclair 
configuration (which has the
advantage not to depend on the exact definition of unreachable) and then 
perhaps a comment
above it explaining the situation.

--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)