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

From: Simone Ballarin <simone.ballarin@bugseng.com>
To: Julien Grall <julien@xen.org>,
	Stefano Stabellini <sstabellini@kernel.org>
Cc: xen-devel@lists.xenproject.org, consulting@bugseng.com,
	Doug Goldstein <cardoe@cardoe.com>,
	Andrew Cooper <andrew.cooper3@citrix.com>,
	George Dunlap <george.dunlap@citrix.com>,
	Jan Beulich <jbeulich@suse.com>, Wei Liu <wl@xen.org>
Subject: Re: [XEN PATCH 2/4] automation/eclair: add deviations and call properties.
Date: Thu, 19 Oct 2023 11:04:12 +0200	[thread overview]
Message-ID: <5b237454-d3e2-4595-82de-59bcfdf1e217@bugseng.com> (raw)
In-Reply-To: <578e282c-0b66-60c1-895f-197a859a1df4@xen.org>

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@bugseng.com>
>>>
>>> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
>>>
>>> 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)