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

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 13/10/2023 11:27, Julien Grall wrote:
> 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...
Well, the implementation of the directive has best-effort precision, 
therefore false positives
like this one are possible. Since Andrew argued that the path is indeed 
safe, I think
it's best to deviate this as such, since other minimal changes could 
also make this one
resurface in the future.

> 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,
I think only conditions are checked to get the possible code paths, to 
have a reasonable
tradeoff between speed and analysis precision. Therefore, it's quite 
possible that it would
give the same caution.

--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)