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

[Bertrand Marquis <Bertrand.Marquis@xxxxxxx>]

> On 28 Sep 2023, at 02:40, Stefano Stabellini <sstabellini@xxxxxxxxxx> wrote:
> 
> 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?
> 

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.