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

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

On Wed, 27 Sep 2023, Bertrand Marquis wrote:
> > On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx> wrote:
> > 
> >>> > 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.
> 
> I agree here and it is easier to make an overall exception where we list the 
> cases
> where this is acceptable (ie all flavors of unreacheable) and document that 
> eclair
> was configured using "xxxx" to handle this.

In that case it looks like we all agree that we can go ahead with this
patch with just the changes to docs/misra/rules.rst to add rule 2.1 and
remove everything else. Which is v2 of this patch:
https://marc.info/?l=xen-devel&m=169283027729298

Henry, can I get one more release-ack for v2 of this patch (only changes
to docs/misra, no code changes)?

Also Bertrand can you provide a formal Ack for v2?


I do think we should have a document to track this kind of deviations
that are not managed by safe.json or exclude-list.json. But I think for
now the rules.rst notes and the ECLAIR config file (which is under
xen.git) will suffice.