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

[Nicola Vetrini <nicola.vetrini@bugseng.com>]

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@xen.org/

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