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

[Simone Ballarin]

On 02/12/23 04:19, Stefano Stabellini wrote:

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.balla...@bugseng.com>

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.

They are not actually deviations, but information that can help
document the code: I suggest creating a new document.

Then, ECLAIR or any other tool will be able to retrieve these properties
directly from this new file.

If you agree I will do it in a separate patch.

But give that the below is OK:
Acked-by: Stefano Stabellini <sstabell...@kernel.org>

---
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

--
Simone Ballarin, M.Sc.

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