On Wed, 27 Sep 2023, Bertrand Marquis wrote:
> > On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetr...@bugseng.com> 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.
