Re: [XEN PATCH][for-4.19 1/9] xen/include: add macro LOWEST_POW2

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 07/10/2023 02:29, Stefano Stabellini wrote:
> On Fri, 6 Oct 2023, Stefano Stabellini wrote:
> > On Fri, 6 Oct 2023, Julien Grall wrote:
> > > Hi Nicola,
> > >
> > > On 06/10/2023 11:34, Nicola Vetrini wrote:
> > > > On 06/10/2023 12:22, Julien Grall wrote:
> > > > > On 06/10/2023 11:02, Nicola Vetrini wrote:
> > > > > > On 06/10/2023 11:29, Julien Grall wrote:
> > > > > > > Hi,
> > > > > > >
> > > > > > > On 06/10/2023 09:26, Nicola Vetrini wrote:
> > > > > > > > The purpose of this macro is to encapsulate the well-known
> > > > > > > > expression
> > > > > > > > 'x & -x', that in 2's complement architectures on unsigned integers
> > > > > > > > will
> > > > > > > > give 2^ffs(x), where ffs(x) is the position of the lowest set bit in
> > > > > > > > x.
> > > > > > > >
> > > > > > > > A deviation for ECLAIR is also introduced.
> > > > > > >
> > > > > > > Can you explain why this is a deviation in ECLAIR rather than one with
> > > > > > > /* SAF-* */ (or whichever name we decide to rename to)? Is this
> > > > > > > because the code is correct from MISRA perspective but the tool is
> > > > > > > confused?
> > > > > > >
> > > > > >
> > > > > > The code does violate Rule 10.1 (a unary minus applied to an unsigned
> > > > > > value is
> > > > > > deemed inappropriate by MISRA), but rather than changing a whole lot of
> > > > > > places where this
> > > > > > construct is used (mainly in x86 code), the reasoning is that it makes
> > > > > > more sense to isolate
> > > > > > it and justify its presence by the fact that on 2's complement
> > > > > > architectures the result is
> > > > > > indeed correct.
> > > > >
> > > > > This is explaining to me why you are adding LOWEST_POW2(). But this
> > > > > doesn't explain why you are not using /* SAF-* */ on top of
> > > > > LOWEST_POW2().
> > > > >
> > > > > To me, we should only use ECLAIR specific deviation when this is a
> > > > > shortcoming with the tool.
> > > > >
> > > > > Cheers,
> > > >
> > > > Because of the way ECLAIR deviation comments work implies that in most cases
> > > > the real
> > > > place where to put the deviation is the usage site
> > > > (the so-called top expansion location of the macro). Now, for widely-used
> > > > macros this is
> > > > cumbersome and would clutter the code unnecessarily. It's way cleaner imo to
> > > > have a single
> > > > line in the configuration with a clear justification that is present in the
> > > > textual output
> > > > of the tool.
> > >
> > > Just to clarify, you are saying that the following would not work for Eclair:
> > >
> > > /* SAF-XXX */
> > > #define LOWEST_POW2()
> > >
> > > Instead you would need the following:
> > >
> > > void foo()
> > > {
> > >    /* SAF-XXX */
> > >    LOWEST()
> > > }
> > >
> > > Am I correct? If so, would something like below (untested) work?
> > >
> > > #define LOWEST_POW2(...) ({ \
> > >    /* SAFE-XXX */           \
> > >    ...
> > >    })
> > >
> > > > But then there are tool interoperability considerations, that would call for
> > > > standardized
> > > > deviation mechanisms, if they do detect this as a violation (which I don't
> > > > know).
> > >
> > > I don't think we need to know whether a tool detects it. We only need to know
> > > whether this is  violation to MISRA. If this is one, then this is a call to
> > > have a marker in the code.
> > >
> > > If this is a false positive, then adding the deviation in the tool
> > > configuration is best (unless there are multiple tools affected).
> > >
> > > >
> > > > In the end, it could be done with a textual deviation, if that's preferred,
> > > > but keep in mind
> > > > that those are more fragile w.r.t. code movement.
> > >
> > > If the comment is around the macro there are limited chance that this will be
> > > missed. But if you are worried about code movement, you should be worried
> > > about macro renaming with your approach (one may not know Eclair has a
> > > deviation) and/or function with the same name.
> > >
> > > I am curious to know what the other thinks.
> >
> > I agree.
> >
> > I think that we should use the SAF-x-safe framework as much as 
> > possible.
> > That is the most flexible and easier to maintain deviation system we
> > have. If we can make it work in this specific case with Julien's
> > suggestion above, then great.
> >
> > But it is becoming clear that the SAF-x-safe framework has 
> > limitations,
> > for instance  https://marc.info/?l=xen-devel&m=169657904027210
> >
> > There are going to be cases where SAF-x-safe won't work. In those 
> > cases,
> > we will probably end up using an ECLAIR specific configuration. Those
> > cases should be hopefully few and should be well documented, also
> > outside of the ECLAIR config file, which is very ECLAIR specific and
> > optimized to be machine readable.
> >
> > We need another RST document under docs/misra to document any 
> > deviations
> > that are not dealt by SAF-x-safe comments. Today we are basically 
> > using
> > the notes section in the docs/misra/rules.rst table but that doesn't
> > scale.
> >
> > So I think we should:
> > - create new RST file like docs/misra/deviations.rst
> > - deviations.rst will list any deviation that is not a SAF-x-safe
> >   deviation
> > - all ECLAIR special deviations in the ECLAIR config file should be
> >   documented in deviations.rst
> > - in the future special ECLAIR deviations in the config file should
> >   come with a new documentation entry in deviations.rst
> >
> >
> > This doesn't entirely address Julien's valid concern but at least it
> > makes it easier to recognize the problem when it occurs.
>
> We already have docs/misra/documenting-violations.rst, so maybe we 
> could
> have one more section at the end of the document with a list of
> "special" deviations.
Sounds good. I'll submit it as part of the ecl updates patch by Simone 
[1].
I think a separate file is better, There's a pointer in rules.rst to
documenting-violations.rst, and a reference to deviations.rst can be 
added here.
[1] https://marc.info/?l=xen-devel&m=169658766432087&w=2

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