Re: [XEN PATCH][for-4.19] domain: add ASSERT to help static analysis tools

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 2023-11-08 09:24, Jan Beulich wrote:
> On 03.11.2023 18:58, Nicola Vetrini wrote:
> > Static analysis tools may detect a possible null
> > pointer dereference at line 760 (the memcpy call)
> > of xen/common/domain.c. This ASSERT helps them in
> > detecting that such a condition is not possible
> > and also provides a basic sanity check.
> I disagree with this being a possible justification for adding such a
> redundant assertion. More detail is needed on what is actually
> (suspected to be) confusing the tool. Plus it also needs explaining
> why (a) adding such an assertion helps and (b) how that's going to
> cover release builds.
How about:
"Static analysis tools may detect a possible null pointer dereference
at line 760 (config->handle) due to config possibly being NULL.

However, given that all system domains, including IDLE, have a NULL
config and in the code path leading to the assertion only real domains
(which have a non-NULL config) can be present."

On point b): this finding is a false positive, therefore even if the 
ASSERT is
expanded to effectively a no-op, there is no inherent problem with Xen's 
code.
The context in which the patch was suggested [1] hinted at avoiding 
inserting in
the codebase false positive comments.

> > --- a/xen/common/domain.c
> > +++ b/xen/common/domain.c
> > @@ -700,6 +700,8 @@ struct domain *domain_create(domid_t domid,
> >
> >      if ( !is_idle_domain(d) )
> >      {
> > +        ASSERT(config);
> > +
> >          watchdog_domain_init(d);
> >          init_status |= INIT_watchdog;
> The assertion being redundant clearly requires it to be accompanied
> by a comment. Otherwise it is going to be a prime subject of
> redundancy elimination.
>
> Jan
Good point; I'd rather keep it short and understandable
(e.g. "This ASSERT helps static analysis tool avoid a false positive
on a possible NULL dereference of config")

[1] 
https://lore.kernel.org/xen-devel/5ddb6398-f2a3-4bcb-8808-bad653b6c3cd@xxxxxxx/
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)