> On 28 Sep 2023, at 02:40, Stefano Stabellini <sstabell...@kernel.org> wrote:
>
> 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?
>
Done, you just need to handle the comment from Julien for it.
Cheers
Bertrand
>
> 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.