Re: [XEN PATCH v2 1/3] automation/eclair: tag function calls to address violations of MISRA C:2012 Rule 13.1

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

On Fri, 24 Nov 2023, Simone Ballarin wrote:
> Rule 13.1: Initializer lists shall not contain persistent side effects
> 
> Invocations of functions in initializer lists cause violations of rule
> 13.1 if the called functions are not tagged with __attribute_pure__ or
> __attribute_const__ as they can produce persistent side effects.
> 
> Handling these violations with  attributes is not always possible: the
> pure and const attributes may cause unwanted and potentially dangerous
> optimisations.
> 
> To avoid this problem ECLAIR allows using the same attributes in the
> -call_properties setting. Additionally, it adds the noeffect attribute
> with the following definition:
> "like pure but can also read volatile variable not triggering side effects"
> 
> These patch tags some functions used in initializer lists to address
> violations of Rule 13.1.
> 
> No functional changes.
> 
> Signed-off-by: Simone Ballarin <simone.ballarin@xxxxxxxxxxx>

Ideally we should also list them somewhere in a document, maybe
docs/misra/deviations.rst? Or a new doc? It would be best if this info
wouldn't only exist in call_properties.ecl.

But give that the below is OK:
Acked-by: Stefano Stabellini <sstabellini@xxxxxxxxxx>


> ---
> Changes in v2:
> New patch partly based on "xen/arm: address violations of MISRA C:2012 Rule 
> 13.1"
> and "xen/include: add pure and const attributes". This new patch uses
> ECL tagging instead of compiler attributes.
> ---
>  .../ECLAIR/call_properties.ecl                | 22 +++++++++++++++++++
>  1 file changed, 22 insertions(+)
> 
> diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl 
> b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> index 3f7794bf8b..c2b2a6182e 100644
> --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
> +++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> @@ -73,6 +73,17 @@
>  -call_properties+={"macro(^va_start$)", {"pointee_write(1=always)", 
> "pointee_read(1=never)", "taken()"}}
>  -call_properties+={"macro(^memcmp$)", {"pointee_write(1..2=never)", 
> "taken()"}}
>  -call_properties+={"macro(^memcpy$)", {"pointee_write(1=always&&2..=never)", 
> "pointee_read(1=never&&2..=always)", "taken()"}}
> +-call_properties+={"name(get_cpu_info)",{pure}}
> +-call_properties+={"name(pdx_to_pfn)",{pure}}
> +-call_properties+={"name(is_pci_passthrough_enabled)",{const}}
> +-call_properties+={"name(get_cycles)", {"noeffect"}}
> +-call_properties+={"name(msi_gflags)",{const}}
> +-call_properties+={"name(hvm_save_size)",{pure}}
> +-call_properties+={"name(cpu_has)",{pure}}
> +-call_properties+={"name(boot_cpu_has)",{pure}}
> +-call_properties+={"name(get_cpu_info)",{pure}}
> +-call_properties+={"name(put_pte_flags)",{const}}
> +-call_properties+={"name(is_pv_vcpu)",{pure}}
>  
>  -doc_begin="Property inferred as a consequence of the semantics of 
> device_tree_get_reg"
>  -call_properties+={"name(acquire_static_memory_bank)", 
> {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}}
> @@ -104,3 +115,14 @@ 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, but they do not produce any persistent 
> side
> +effect."
> +-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {noeffect}}
> +-doc_end
> +
> +-doc_begin="Functions generated by TYPE_SAFE are const."
> +-call_properties+={"^(mfn|gfn|pfn)_x\\(.*$",{const}}
> +-call_properties+={"^_(mfn|gfn|pfn)\\(.*$",{const}}
> +-doc_end
> -- 
> 2.34.1
>