Re: [XEN PATCH v2 05/13] x86/traps: address violations of MISRA C Rule 16.3

[Jan Beulich <jbeulich@xxxxxxxx>]

On 26.06.2024 03:11, Stefano Stabellini wrote:
> On Tue, 25 Jun 2024, Jan Beulich wrote:
>> On 25.06.2024 02:54, Stefano Stabellini wrote:
>>> On Mon, 24 Jun 2024, Federico Serafini wrote:
>>>> Add break or pseudo keyword fallthrough to address violations of
>>>> MISRA C Rule 16.3: "An unconditional `break' statement shall terminate
>>>> every switch-clause".
>>>>
>>>> No functional change.
>>>>
>>>> Signed-off-by: Federico Serafini <federico.serafini@xxxxxxxxxxx>
>>>> ---
>>>>  xen/arch/x86/traps.c | 3 +++
>>>>  1 file changed, 3 insertions(+)
>>>>
>>>> diff --git a/xen/arch/x86/traps.c b/xen/arch/x86/traps.c
>>>> index 9906e874d5..cbcec3fafb 100644
>>>> --- a/xen/arch/x86/traps.c
>>>> +++ b/xen/arch/x86/traps.c
>>>> @@ -1186,6 +1186,7 @@ void cpuid_hypervisor_leaves(const struct vcpu *v, 
>>>> uint32_t leaf,
>>>>  
>>>>      default:
>>>>          ASSERT_UNREACHABLE();
>>>> +        break;
>>>
>>> Please add ASSERT_UNREACHABLE to the list of "unconditional flow control
>>> statements" that can terminate a case, in addition to break.
>>
>> Why? Exactly the opposite is part of the subject of a recent patch, iirc.
>> Simply because of the rules needing to cover both debug and release builds.
> 
> The reason is that ASSERT_UNREACHABLE() might disappear from the release
> build but it can still be used as a marker during static analysis. In
> my view, ASSERT_UNREACHABLE() is equivalent to a noreturn function call
> which has an empty implementation in release builds.
> 
> The only reason I can think of to require a break; after an
> ASSERT_UNREACHABLE() would be if we think the unreachability only apply
> to debug build, not release build:
> 
> - debug build: it is unreachable
> - release build: it is reachable
> 
> I don't think that is meant to be possible so I think we can use
> ASSERT_UNREACHABLE() as a marker.

Well. For one such an assumption takes as a prereq that a debug build will
be run through full coverage testing, i.e. all reachable paths proven to
be taken. I understand that this prereq is intended to somehow be met,
even if I'm having difficulty seeing how such a final proof would look
like: Full coverage would, to me, mean that _every_ line is reachable. Yet
clearly any ASSERT_UNREACHABLE() must never be reached.

And then not covering for such cases takes the further assumption that
debug and release builds are functionally identical. I'm afraid this would
be a wrong assumption to make:
1) We may screw up somewhere, with code wrongly enabled only in one of the
   two build modes.
2) The compiler may screw up, in particular with optimization.

Jan