Re: [XEN PATCH v2] domain: add ASSERT to help static analysis tools

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 2023-11-17 10:21, Nicola Vetrini wrote:
> Static analysis tools may detect a possible null pointer
> dereference of 'config'. This ASSERT helps them in detecting
> that such a condition is not possible given that only
> real domains can enter this branch, which are guaranteeed to have
> a non-NULL config at this point, but this information is not
> inferred by the tool.
>
> Checking that the condition given in the assertion holds via
> testing is the means to protect release builds, where the assertion
> expands to effectively nothing.
>
> Suggested-by: Julien Grall <julien@xxxxxxx>
> Signed-off-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> Acked-by: Stefano Stabellini <sstabellini@xxxxxxxxxx>
> ---
> Changes in v2:
> - Clarified the context in which the assertion is useful.
>
> The check may be later improved by proper error checking
> instead of relying on the semantics explained here:
> https://lore.kernel.org/xen-devel/61f04d4b-34d9-4fd1-a989-56b042b4f3d8@xxxxxxxxxx/
> ---
>  xen/common/domain.c | 7 +++++++
>  1 file changed, 7 insertions(+)
>
> diff --git a/xen/common/domain.c b/xen/common/domain.c
> index 8f9ab01c0cb7..924099db1098 100644
> --- a/xen/common/domain.c
> +++ b/xen/common/domain.c
> @@ -700,6 +700,13 @@ struct domain *domain_create(domid_t domid,
>
>      if ( !is_idle_domain(d) )
>      {
> +        /*
> +         * The assertion helps static analysis tools infer that config 
> cannot
> +         * be NULL in this branch, which in turn means that it can be 
> safely
> +         * dereferenced. Therefore, this assertion is not redundant.
> +         */
> +        ASSERT(config);
> +
>          watchdog_domain_init(d);
>          init_status |= INIT_watchdog;
This patch has been revised according to the comments received on v1 to 
clarify that the assertion seems redundant, but it's useful for other 
purposes.
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)