Re: [XEN PATCH 10/11] xen/sched: add ASSERT_UNREACHABLE() to address MISRA C:2012 Rule 2.1

[Jan Beulich <jbeulich@xxxxxxxx>]

On 08.08.2023 23:14, Stefano Stabellini wrote:
> On Tue, 8 Aug 2023, Julien Grall wrote:
>> On 08/08/2023 16:53, Nicola Vetrini wrote:
>>>>> ... "return" alone already tells the compiler that "break" is
>>>>> unreachable. You don't need unreachable() for that. As said before,
>>>>> "break" like this simply want purging (and Misra is wrong to demand
>>>>> "break" everywhere - it should instead demand no [unannotated]
>>>>> fall-through, which can also be achieved by return, continue, and
>>>>> goto).
>>>>
>>>> My suggestion was in the context of this series where we add
>>>> ASSERT_UNREACHABLE() before break. From my understanding, we don't
>>>> have a lot of leeway here because, from what Nicola wrote, rule 16.3
>>>> is mandatory.
>>>>
>>>> So I think using unreachable is better if we every decide to use break
>>>> after return.
>>>>
>>>> Cheers,
>>>
>>> 16.3 is not Mandatory, just Required.
>>
>> Ah I misread what you wrote. In that case...
>>
>>> I was just reluctant to knowingly add one more violation
>>> while fixing another before submitting the patch. If indeed 16.3 won't
>>> likely be adopted by Xen,
>>> then that break should indeed go away.
>>>
>>> However, the main thing that's holding me back from doing a slimmed-down v2
>>> here is that
>>> evidently there's no consensus even on the ASSERT_UNREACHABLE() patches.
>>
>> ... I agree with the following statement from Jan:
>>
>> "it should instead demand no [unannotated] fall-through, which can also be
>> achieved by return, continue, and goto"
> 
> I also think it is a better idea to have no unannotated fall-through in
> switch statements (unless we have a "case" with nothing underneath, so
> two cases next to each other). In other words the following are all OK
> in my view:
> 
>   case A:
>     do();
>     break;
>   case B:
>     do();
>     return true;
>   case Ca:
>   case Cb:
>     goto fail;
>   case D:
>     i++;
>     continue;
>   case E:
>     do();
>     /* fall-through */
>   case F:
>     do();
>     break;
> 
> While the following is not OK:
> 
>   case A:
>     do();
>   case B:
>     do();
> 
> This should be what we already do in Xen, although it is not documented
> properly. Jan, Julien do you agree?

Yes.

> If so, could Eclair be configured to check for this pattern (or
> similar)?
> 
> We must have one of the following:
> - break, continue, return, goto
> - /* fall-through */

- fallthrough;

(the pseudo keyword that we have; see compiler.h for actually having the
documentation you're looking for, albeit missing "continue", and of
course not really expected to live [just] there)

Jan

> - empty case body (case Ca/Cb)