Re: MISRA C:2012 D4.11 caution on staging

[Andrew Cooper <andrew.cooper3@xxxxxxxxxx>]

On 11/10/2023 3:47 pm, Nicola Vetrini wrote:
> On 11/10/2023 02:15, Andrew Cooper wrote:
>> On 10/10/2023 5:31 pm, Nicola Vetrini wrote:
>>> Hi,
>>>
>>> as you can see from [1], there's a MISRA C guideline, D4.11, that is
>>> supposed to be clean
>>> (i.e., have no reports), but has a caution on an argument to memcpy
>>> (the second argument might be null according to the checker, given a
>>> set of assumptions on
>>> the control flow). To access the report just click on the second link
>>> in the log, which should take you to a webpage with a list of
>>> MISRA guidelines. Click on D4.11 and you'll see the full report, which
>>> I pasted below for convenience.
>>>
>>> If the finding is genuine, then some countermeasure needs to be taken
>>> against this
>>> possible bug, otherwise it needs to be motivated why the field
>>> config->handle can't
>>> be null at that point.
>>> The finding is likely the result of an improvement made to the
>>> checker, because the first
>>> analysis I can see that spots it happened when rc1 has been tagged,
>>> but that commit does not
>>> touch the involved files.
>>>
>>> [1] https://gitlab.com/xen-project/xen/-/jobs/5251222578
>>
>> That's a false positive, but I'm not entirely surprised that the checker
>> struggled to see it.
>>
>> First,
>>
>> ASSERT(is_system_domain(d) ? config == NULL : config != NULL);
>>
>> All system domains (domid >= 0x7ff0, inc IDLE) pass a NULL config.  All
>> other domains pass a real config.
>>
>> Next,
>>
>> /* DOMID_{XEN,IO,etc} (other than IDLE) are sufficiently constructed. */
>> if ( is_system_domain(d) && !is_idle_domain(d) )
>>     return d;
>>
>> So at this point we only have the IDLE domain and real domains.
>>
>> And finally, the complained-about construct is inside an:
>>
>> if ( !is_idle_domain(d) )
>>     ...
>>
>> hence config cannot be NULL, but only because of the way in which
>> is_{system,idle}_domain() interact.
>>
>> ~Andrew
>
> Ok. I think this should be documented as a false positive using the
> comment deviation mechanism
> in the false-positive-eclair.json file (once a name for the prefix is
> settled on in the
> other thread).
>

Yeah - I was expecting that.

This code is mid-cleanup (in my copious free time, so not for several
releases now...) but even when it is rearranged sufficiently for IDLE to
have an earlier exit, I still wouldn't expect a static analyser to be
able to recognise this as being safe.

~Andrew