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

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

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.