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

[Julien Grall <julien@xxxxxxx>]

Hi Nicola,

On 13/10/2023 16:11, Nicola Vetrini wrote:
> 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.
If Eclair always reported the false positive, then I would have agree 
that deviating would make sense. But you said this was due to an 
improvement in the checker.
I expect improvement in the checker to reduce the number of false 
positive, not introducing new ones. So I think we need to understand 
what changed.
> > 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.
What I want to avoid is adding a SAF-* every time there are an update to 
Eclair that reports more false positive. This will make the code more 
difficult to read.
Instead, it would be best to find a way to help Eclair to detect this is 
not an issue and also improve readability. Would the following help Eclair?
diff --git a/xen/common/domain.c b/xen/common/domain.c
index 30c227967345..ab16124eabd6 100644
--- a/xen/common/domain.c
+++ b/xen/common/domain.c
@@ -671,6 +671,8 @@ struct domain *domain_create(domid_t domid,

     if ( !is_idle_domain(d) )
     {
+        ASSERT(config);
+
         watchdog_domain_init(d);
         init_status |= INIT_watchdog;

Cheers,

--
Julien Grall