Re: [PATCH v1] misra: add deviation of Rule 10.1 for unary minus

[Julien Grall <julien@xxxxxxx>]

Hi Nicola,

On 23/04/2025 22:09, Nicola Vetrini wrote:
> On 2025-04-23 22:48, Julien Grall wrote:
> > Hi Victor,
> >
> > On 23/04/2025 18:54, victorm.lira@xxxxxxx wrote:
> > > From: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> > >
> > > MISRA C Rule 10.1 states:
> > > "Operands shall not be of an inappropriate essential type"
> > >
> > > The unary minus operator applied to an unsigned quantity has
> > > a semantics (wrap around) that is well-known to all Xen developers.
> > > Thus, this operation is deemed safe.
> > >
> > > No functional change.
> > >
> > > Signed-off-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> > > Signed-off-by: Federico Serafini <federico.serafini@xxxxxxxxxxx>
> > > Signed-off-by: Victor Lira <victorm.lira@xxxxxxx>
> > > ---
> > > Changes v1:
> > > - add rule title to commit message
> > > ---
> > > Cc: Andrew Cooper <andrew.cooper3@xxxxxxxxxx>
> > > Cc: Anthony PERARD <anthony.perard@xxxxxxxxxx>
> > > Cc: Michal Orzel <michal.orzel@xxxxxxx>
> > > Cc: Jan Beulich <jbeulich@xxxxxxxx>
> > > Cc: Julien Grall <julien@xxxxxxx>
> > > Cc: Roger Pau Monné <roger.pau@xxxxxxxxxx>
> > > Cc: Stefano Stabellini <sstabellini@xxxxxxxxxx>
> > > Cc: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> > > Cc: Federico Serafini <federico.serafini@xxxxxxxxxxx>
> > > Cc: Bertrand Marquis <bertrand.marquis@xxxxxxx>
> > > ---
> > >   automation/eclair_analysis/ECLAIR/deviations.ecl | 6 ++++++
> > >   docs/misra/deviations.rst                        | 6 ++++++
> > >   2 files changed, 12 insertions(+)
> > >
> > > diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/ 
> > > automation/eclair_analysis/ECLAIR/deviations.ecl
> > > index 303b06203a..2cfce850bd 100644
> > > --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> > > +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > > @@ -347,6 +347,12 @@ constant expressions are required.\""
> > >     "any()"}
> > >   -doc_end
> > >
> > > +-doc_begin="Unary minus operations on non-negative integers have a 
> > > semantics (wrap around) that is well-known to all Xen developers."
> > > +-config=MC3A2.R10.1,etypes+={safe,
> > > +  "stmt(node(unary_operator)&&operator(minus))",
> > > +  "src_expr(definitely_in(0..))"}
> > > +-doc_end
> > > +
> > >   #
> > >   # Series 11
> > >   #
> > > diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> > > index cfdd1a9838..c5897e31c5 100644
> > > --- a/docs/misra/deviations.rst
> > > +++ b/docs/misra/deviations.rst
> > > @@ -321,6 +321,12 @@ Deviations related to MISRA C:2012 Rules:
> > >          If no bits are set, 0 is returned.
> > >        - Tagged as `safe` for ECLAIR.
> > >
> > > +   * - R10.1
> > > +     - Applying the unary minus operator to an unsigned quantity has a
> > > +       semantics (wrap around) that is well-known to all Xen 
> > > developers.
> > > +       For this reason, the operation is safe.
> > I have realized we use similar wording in the rest of the deviations, 
> > but this is rather fragile argument. "well-known" is very subjective 
> > and could change over time.
> > How many violations do we have? Could we deviate them one by one?
> Hi Julien,
>
> around 10 on ARM, but more than 100 on x86 scattered around multiple 
> constructs (e.g. not only inside a handful of macros), so I don't think 
> it's feasible to deviate them one by one. 
Interesting. This seems to contradict what Stefano just wrote:

"
We only have few instances of this pattern and the few we have are well
understood and certainly deliberate.
"

> I do agree that the wording is 
> subjective, but it is rather well-defined which toolchains and 
> architectures are used (C-language-toolchain.rst). Perhaps a wording 
> mentioning the specific assumptions implied here can address your concerns?
If this is well-defined by the toolchains/architectures, then it is a 
better argument than "Xen community knows it".
Cheers,

--
Julien Grall