Re: [XEN PATCH 2/4] automation/eclair: add deviations and call properties.

[Simone Ballarin <simone.ballarin@xxxxxxxxxxx>]

On 19/10/23 10:26, Julien Grall wrote:
> Hi Simone,
>
> On 19/10/2023 08:44, Simone Ballarin wrote:
> > On 19/10/23 02:57, Stefano Stabellini wrote:
> > > On Wed, 18 Oct 2023, Simone Ballarin wrote:
> > > > Deviate violations of MISRA C:2012 Rule 13.1 caused by
> > > > functions vcpu_runnable and __bad_atomic_size. These functions
> > > > contain side-effects such as debugging logs, assertions and
> > > > failures that cannot cause unexpected behaviors.
> > > >
> > > > Add "noeffect" call property to functions read_u.*_atomic and
> > > > get_cycles.
> > > >
> > > > Signed-off-by: Simone Ballarin <simone.ballarin@xxxxxxxxxxx>
> > > Acked-by: Stefano Stabellini <sstabellini@xxxxxxxxxx>
> > >
> > > However one comment below
> > >
> > >
> > > > ---
> > > >   .../eclair_analysis/ECLAIR/call_properties.ecl      | 10 ++++++++++
> > > >   automation/eclair_analysis/ECLAIR/deviations.ecl    | 13 
> > > > +++++++++++++
> > > >   docs/misra/deviations.rst                           | 11 +++++++++++
> > > >   3 files changed, 34 insertions(+)
> > > >
> > > > diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl 
> > > > b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> > > > index 3f7794bf8b..f410a6aa58 100644
> > > > --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
> > > > +++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> > > > @@ -104,3 +104,13 @@ Furthermore, their uses do initialize the 
> > > > involved variables as needed by futher
> > > > -call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", 
> > > > {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> > > > -call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", 
> > > > {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> > > >   -doc_end
> > > > +
> > > > +-doc_begin="Functions generated by build_atomic_read cannot be 
> > > > considered pure
> > > > +since the input pointer is volatile."
> > > > +-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {"noeffect"}}
> > > > +-doc_end
> > > > +
> > > > +-doc_begin="get_cycles does not perform visible side-effects "
> > > > +-call_property+={"name(get_cycles)", {"noeffect"}}
> > > > +-doc_end
> > > > +
> > > > diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl 
> > > > b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > > > index fa56e5c00a..b80ccea7bc 100644
> > > > --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> > > > +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > > > @@ -233,6 +233,19 @@ this."
> > > >   -config=MC3R1.R10.1,etypes+={safe,
> > > > "stmt(operator(and||or||xor||not||and_assign||or_assign||xor_assign))",
> > > >     "any()"}
> > > > +#
> > > > +# Series 13.
> > > > +#
> > > > +
> > > > +-doc_begin="Function __bad_atomic_size is intended to generate a 
> > > > linkage error
> > > > +if invoked. Calling it in intentionally unreachable switch cases is 
> > > > safe even
> > > > +in a initializer list."
> > > > +-config=MC3R1.R13.1,reports+={safe, 
> > > > "first_area(^.*__bad_atomic_size.*$)"}
> > > > +-doc_end
> > > > +
> > > > +-doc_begin="Function vcpu_runnable contains pragmas and other 
> > > > side-effects for
> > > > +debugging purposes, their invocation is safe even in a initializer 
> > > > list."
> > > > +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*vcpu_runnable.*$)"}
> > > >   -doc_end
> > > >   -doc_begin="See Section \"4.5 Integers\" of \"GCC_MANUAL\", where 
> > > > it says that
> > > > diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> > > > index 8511a18925..2fcdb8da58 100644
> > > > --- a/docs/misra/deviations.rst
> > > > +++ b/docs/misra/deviations.rst
> > > > @@ -192,6 +192,17 @@ Deviations related to MISRA C:2012 Rules:
> > > >          See automation/eclair_analysis/deviations.ecl for the full 
> > > > explanation.
> > > >        - Tagged as `safe` for ECLAIR.
> > > > +   * - R13.1
> > > > +     - Function __bad_atomic_size is intended to generate a linkage 
> > > > error if
> > > > +       invoked. Calling it in intentionally unreachable switch 
> > > > cases is
> > > > +       safe even in a initializer list.
> > > > +     - Tagged as `safe` for ECLAIR.
> > > > +
> > > > +   * - R13.1
> > > > +     - Function vcpu_runnable contains pragmas and other 
> > > > side-effects for
> > > > +       debugging purposes, their invocation is safe even in a 
> > > > initializer list.
> > > > +     - Tagged as `safe` for ECLAIR.
> > >
> > > Would it be possible to use SAF instead? If not, this is fine.
> > Yes, but I do not suggest using SAF comments in these cases.
> There are not many use of __bad_atomic_size() and I don't expect much 
> more. So I think SAF- makes more sense.
There are 13 invocations in the preprocessed code: some of them are 
contained in macro expansions. Adding a SAF in a macro means to add 
useless comments if the macro is not expanded in an initializer list.
The correct thing would be adding 13 SAFs. If this is ok, I can do it.

> For vcpu_runnable(), I don't quite understand the argument. I can't find 
> any pragma around the function and I can't find any side-effects in it. 
> Can you clarify?

vcpu_runnable calls atomic_read.

In ARM, atomic_read uses a volatile pointer (that's a side-effect).

In X86 it contains a MACRO (read_atomic) that contains the pragmas
and also __bad_atomic_size.

Maybe the text should discriminate the two cases.

> Cheers,
--
Simone Ballarin, M.Sc.

Field Application Engineer, BUGSENG (https://bugseng.com)