Re: [XEN PATCH] x86: p2m-pod: address violation of MISRA C Rule 2.1

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 2024-06-28 01:18, Stefano Stabellini wrote:
> On Thu, 27 Jun 2024, Nicola Vetrini wrote:
> > The label 'out_unmap' is only reachable after ASSERT_UNREACHABLE,
> > so the code below is only executed upon erroneously reaching that
> > program point and calling domain_crash, thus resulting in the
> > for loop after 'out_unmap' to become unreachable in some 
> > configurations.
> > This is a defensive coding measure to have a safe fallback that is
> > reachable in non-debug builds, and can thus be deviated with a
> > comment-based deviation.
> >
> > No functional change.
> >
> > Signed-off-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> The patch needs rebasing as it doesn't apply to staging anymore
>
> Other than that:
>
> Reviewed-by: Stefano Stabellini <sstabellini@xxxxxxxxxx>
>
> This is actually going help also in terms of identifying impossible 
> code
> paths for coverage
Thanks, I just sent a rebased v2 version.

> > ---
> >  docs/misra/safe.json      | 8 ++++++++
> >  xen/arch/x86/mm/p2m-pod.c | 1 +
> >  2 files changed, 9 insertions(+)
> >
> > diff --git a/docs/misra/safe.json b/docs/misra/safe.json
> > index c213e0a0be3b..b114c9485c86 100644
> > --- a/docs/misra/safe.json
> > +++ b/docs/misra/safe.json
> > @@ -60,6 +60,14 @@
> >          },
> >          {
> >              "id": "SAF-7-safe",
> > +            "analyser": {
> > +                "eclair": "MC3R1.R2.1"
> > +            },
> > +            "name": "MC3R1.R2.1: statement unreachable in some 
> > configurations",
> > +            "text": "Every path that can reach this statement is 
> > preceded by statements that make it unreachable in certain 
> > configurations (e.g. ASSERT_UNREACHABLE). This is understood as a 
> > means of defensive programming."
> > +        },
> > +        {
> > +            "id": "SAF-8-safe",
> >              "analyser": {},
> >              "name": "Sentinel",
> >              "text": "Next ID to be used"
> > diff --git a/xen/arch/x86/mm/p2m-pod.c b/xen/arch/x86/mm/p2m-pod.c
> > index bd84fe9e27ee..5a96c46a2286 100644
> > --- a/xen/arch/x86/mm/p2m-pod.c
> > +++ b/xen/arch/x86/mm/p2m-pod.c
> > @@ -1040,6 +1040,7 @@ out_unmap:
> >       * Something went wrong, probably crashing the domain.  Unmap
> >       * everything and return.
> >       */
> > +    /* SAF-7-safe Rule 2.1: defensive programming */
> >      for ( i = 0; i < count; i++ )
> >          if ( map[i] )
> >              unmap_domain_page(map[i]);
> > --
> > 2.34.1
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)