[XEN PATCH] xen/arm: p2m: refactor 'p2m_get_entry'

Nicola Vetrini posted 1 patch 9 months, 1 week ago
Patches applied successfully (tree, apply log)
git fetch https://gitlab.com/xen-project/patchew/xen tags/patchew/118566cd8b9ebbcedd2b610f5f602cc31c12fd55.1689922099.git.nicola.vetrini@bugseng.com
xen/arch/arm/p2m.c | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
[XEN PATCH] xen/arm: p2m: refactor 'p2m_get_entry'
Posted by Nicola Vetrini 9 months, 1 week ago
This function is refactored to avoid using a
local dummy variable that served as a fallback
if the parameter 't' is NULL.

Storing the address of that variable into 't' caused
static analysis tools not to be able to recognize the
validity of the initialization, and to help with automatic
checking the two usages of 't' have been slightly refactored.

No functional changes.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
Suggested-by: Julien Grall <julien@xen.org>
---
 xen/arch/arm/p2m.c | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/xen/arch/arm/p2m.c b/xen/arch/arm/p2m.c
index de32a2d638..05d65db01b 100644
--- a/xen/arch/arm/p2m.c
+++ b/xen/arch/arm/p2m.c
@@ -496,16 +496,13 @@ mfn_t p2m_get_entry(struct p2m_domain *p2m, gfn_t gfn,
     lpae_t entry, *table;
     int rc;
     mfn_t mfn = INVALID_MFN;
-    p2m_type_t _t;
     DECLARE_OFFSETS(offsets, addr);
 
     ASSERT(p2m_is_locked(p2m));
     BUILD_BUG_ON(THIRD_MASK != PAGE_MASK);
 
-    /* Allow t to be NULL */
-    t = t ?: &_t;
-
-    *t = p2m_invalid;
+    if ( t )
+        *t = p2m_invalid;
 
     if ( valid )
         *valid = false;
@@ -549,7 +546,8 @@ mfn_t p2m_get_entry(struct p2m_domain *p2m, gfn_t gfn,
 
     if ( p2m_is_valid(entry) )
     {
-        *t = entry.p2m.type;
+        if ( t )
+            *t = entry.p2m.type;
 
         if ( a )
             *a = p2m_mem_access_radix_get(p2m, gfn);
-- 
2.34.1
Re: [XEN PATCH] xen/arm: p2m: refactor 'p2m_get_entry'
Posted by Julien Grall 9 months, 1 week ago
Hi Nicola,

I would add "to please ECLAIR" in the commit title.

On 21/07/2023 07:49, Nicola Vetrini wrote:
> This function is refactored to avoid using a
> local dummy variable that served as a fallback
> if the parameter 't' is NULL.
> 
> Storing the address of that variable into 't' caused
> static analysis tools not to be able to recognize the

Can you mention which static analysis tools is not happy and the 
version? This could help us in the future if we decided to revert the patch.

> validity of the initialization, and to help with automatic
> checking the two usages of 't' have been slightly refactored.
> 
> No functional changes.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> Suggested-by: Julien Grall <julien@xen.org>
> ---
>   xen/arch/arm/p2m.c | 10 ++++------
>   1 file changed, 4 insertions(+), 6 deletions(-)
> 
> diff --git a/xen/arch/arm/p2m.c b/xen/arch/arm/p2m.c
> index de32a2d638..05d65db01b 100644
> --- a/xen/arch/arm/p2m.c
> +++ b/xen/arch/arm/p2m.c
> @@ -496,16 +496,13 @@ mfn_t p2m_get_entry(struct p2m_domain *p2m, gfn_t gfn,
>       lpae_t entry, *table;
>       int rc;
>       mfn_t mfn = INVALID_MFN;
> -    p2m_type_t _t;
>       DECLARE_OFFSETS(offsets, addr);
>   
>       ASSERT(p2m_is_locked(p2m));
>       BUILD_BUG_ON(THIRD_MASK != PAGE_MASK);
>   
> -    /* Allow t to be NULL */
> -    t = t ?: &_t;
> -
> -    *t = p2m_invalid;
> +    if ( t )
> +        *t = p2m_invalid;
>   
>       if ( valid )
>           *valid = false;
> @@ -549,7 +546,8 @@ mfn_t p2m_get_entry(struct p2m_domain *p2m, gfn_t gfn,
>   
>       if ( p2m_is_valid(entry) )
>       {
> -        *t = entry.p2m.type;
> +        if ( t )
> +            *t = entry.p2m.type;
>   
>           if ( a )
>               *a = p2m_mem_access_radix_get(p2m, gfn);

Cheers,

-- 
Julien Grall
Re: [XEN PATCH] xen/arm: p2m: refactor 'p2m_get_entry'
Posted by Nicola Vetrini 9 months, 1 week ago

On 21/07/23 12:01, Julien Grall wrote:
> Hi Nicola,
> 
> I would add "to please ECLAIR" in the commit title.

I would be against this. It's the MISRA assessor that needs
to understand and agree on what has been done to claim MISRA compliance. 
A static analysis tool is just a useful way to help reaching this aim.

> 
> On 21/07/2023 07:49, Nicola Vetrini wrote:
>> This function is refactored to avoid using a
>> local dummy variable that served as a fallback
>> if the parameter 't' is NULL.
>>
>> Storing the address of that variable into 't' caused
>> static analysis tools not to be able to recognize the
> 
> Can you mention which static analysis tools is not happy and the 
> version? This could help us in the future if we decided to revert the 
> patch.
> 

It is not a matter of tool happiness, but of MISRA compliance.
There are several tools (even emblazoned ones) that have lots
of false negatives, also for mandatory guidelines such as Rule 9.1:
the fact that they do not issue messages for possible violations
they cannot exclude is happiness for nobody (especially for those
who have to ensure there are indeed no violations). Two things
that have to be kept well in mind are:

1) Rule 9.1 is undecidable, there will never be a tool that flags all
    and only the violations; tools will false positives, false negatives
    or both. ECLAIR (all versions of it) errs on the safe side.

2) Safety-critical code has to be boring and obviously correct:
    programming virtuosism and safety are in two very different leagues.
    This is why ECLAIR uses the algorithm it uses: typically when it
    issues a caution the code is not obviously correct.

Kind Regards,

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)
Re: [XEN PATCH] xen/arm: p2m: refactor 'p2m_get_entry'
Posted by Julien Grall 9 months, 1 week ago

On 24/07/2023 14:15, Nicola Vetrini wrote:
> 
> 
> On 21/07/23 12:01, Julien Grall wrote:
>> Hi Nicola,
>>
>> I would add "to please ECLAIR" in the commit title.
> 
> I would be against this. It's the MISRA assessor that needs
> to understand and agree on what has been done to claim MISRA compliance. 
> A static analysis tool is just a useful way to help reaching this aim.

I have already mentioned in [1], but I will repeat here in a shorter 
version. If Eclair wasn't complaining about it, then this is not a patch 
I would have accepted with the current justification.

>
>>
>> On 21/07/2023 07:49, Nicola Vetrini wrote:
>>> This function is refactored to avoid using a
>>> local dummy variable that served as a fallback
>>> if the parameter 't' is NULL.
>>>
>>> Storing the address of that variable into 't' caused
>>> static analysis tools not to be able to recognize the
>>
>> Can you mention which static analysis tools is not happy and the 
>> version? This could help us in the future if we decided to revert the 
>> patch.
>>
> 
> It is not a matter of tool happiness, but of MISRA compliance.
 From my understanding, the code you are modifying is compliant with 
MISRA. So you are only doing this patch to:

   1) Help Eclair to figure out there is no issue
   2) Avoid adding an explanation in the documentation why this is safe

> There are several tools (even emblazoned ones) that have lots
> of false negatives, also for mandatory guidelines such as Rule 9.1:
> the fact that they do not issue messages for possible violations
> they cannot exclude is happiness for nobody (especially for those
> who have to ensure there are indeed no violations). Two things
> that have to be kept well in mind are:

My point is that someone in the future may decide to use a tool that 
will complain about your change here. A possible course of action would 
be to revert the patch but this would not work for Eclair.

By explicitly mentioning Eclair in the commit message/title, you are 
making a statement that a simple revert would not work. This will save a 
lot of back and forth, including arguments on the ML.

Cheers,

-- 
Julien Grall