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

[Julien Grall <julien@xxxxxxx>]

Hi Andrew,

On 11/10/2023 08:51, Andrew Cooper wrote:
> 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.
Looking through the analysis, I think Eclair properly detect the IDLE 
domain. But it thinks the domain ID has changed mid function (see my 
other reply to Stefano).
So we can return early for the IDLE domain, then this should silence 
Eclair. That said, it is unclear to me why it thinks the domain_id can 
change...
A simple way to fix it would be to have a local boolean that will be 
used in place of is_idle_domain(d). This should help Eclair to detect 
that a domain cannot change its ID in the middle of domain construction.
Cheers,

--
Julien Grall