[XEN PATCH v4 0/4] address violation of MISRA C:2012 Rule 13.1

[XEN PATCH v4 0/4] address violation of MISRA C:2012 Rule 13.1

[Simone Ballarin]

The Xen sources contain violations of MISRA C:2012 Rule 13.1 whose headline states:
"Initializer lists shall not contain persistent side effects".

The file properties.json containing function and macro properties is introduced, as
stated in v2 discussion. Some functions and macros are found to have properties that
can be exploited by static analyzers. For this reason, the file docs/properties.json
contains all the needed properties. A description of the json file is documented in
docs/properties.rst.

Some persistent effects have been moved outside initializer lists to address violations
of Rule 13.1.

Link to the discussion: https://lore.kernel.org/all/cover.1700844359.git.simone.ballarin@bugseng.com/T/#u

Changes in v4:
- added missing script for converting function_macro_properties.json in ECL configurations
  and other related improvements.

Changes in v3:
- change prefix from xen to xen/ns16550
- add assignment of rc in xen/ns16550
- use rc as controlling expression in the following if-statement
- change commit prefix from xen/arm to xen
- specify where saf-3-safe comments are applied in guestcopy.c
- reword saf comments text

Maria Celeste Cesario (1):
  eclair: move function and macro properties outside ECLAIR

Simone Ballarin (3):
  xen: add SAF deviation for debugging and logging effects
  xen/ns16550: address violations of MISRA C:2012 Rule 13.1
  xen/x86: address violations of MISRA C:2012 Rule 13.1

 .../eclair_analysis/ECLAIR/analysis.ecl       |   1 +
 .../ECLAIR/call_properties.ecl                | 128 ---
 automation/eclair_analysis/prepare.sh         |   2 +
 automation/eclair_analysis/propertyparser.py  |  37 +
 docs/function_macro_properties.json           | 841 ++++++++++++++++++
 docs/function_macro_properties.rst            |  58 ++
 docs/misra/safe.json                          |  16 +
 xen/arch/arm/device.c                         |   1 +
 xen/arch/arm/guestcopy.c                      |  16 +-
 xen/arch/x86/hvm/hvm.c                        |   1 +
 xen/arch/x86/io_apic.c                        |   9 +-
 xen/arch/x86/mpparse.c                        |   3 +-
 xen/arch/x86/setup.c                          |   3 +-
 xen/common/sched/core.c                       |   3 +
 xen/drivers/char/ns16550.c                    |   4 +-
 15 files changed, 985 insertions(+), 138 deletions(-)
 delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl
 create mode 100644 automation/eclair_analysis/propertyparser.py
 create mode 100644 docs/function_macro_properties.json
 create mode 100644 docs/function_macro_properties.rst

-- 
2.34.1

[XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Simone Ballarin]

Rule 13.1: Initializer lists shall not contain persistent side effects

Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
of logging effects is always safe.

Function hvm_get_guest_tsc_fixed (indirectly) performs different side effects.
For example it calls hvm_get_guest_time_fixed that contains an ASSERT and calls
to spin_lock and spin_unlock.

These side effects are not dangerous: they can be executed regardless of the
initializer list evaluation order

This patch deviates violations using SAF commits caused by debug/logging macros and
functions.

Asm volatile statements in initializer lists that do not perform any persistent side
effect are safe: this patch deviates violations caused by uses of the current macro
(that contains an asm volatile) in initializer lists.

No functional changes.

Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>

---
Changes in v3:
- change commit prefix from xen/arm to xen
- specify where saf-3-safe comments are applied in guestcopy.c
- reword SAF text
Changes in v2:
New patch based on the discussion for "xen/arm: address violations of MISRA C:2012 Rule 13.1".
---
 docs/misra/safe.json     | 16 ++++++++++++++++
 xen/arch/arm/device.c    |  1 +
 xen/arch/arm/guestcopy.c | 16 ++++++++++++----
 xen/arch/x86/hvm/hvm.c   |  1 +
 xen/common/sched/core.c  |  3 +++
 5 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/docs/misra/safe.json b/docs/misra/safe.json
index 952324f85c..5539e8dfda 100644
--- a/docs/misra/safe.json
+++ b/docs/misra/safe.json
@@ -28,6 +28,22 @@
         },
         {
             "id": "SAF-3-safe",
+            "analyser": {
+                "eclair": "MC3R1.R13.1"
+            },
+            "name": "MC3R1.R13.1: effects for debugging and logging",
+            "text": "Effects for debugging and loggings reasons that crash execution or produce logs are allowed in initializer lists. The evaluation order in abnormal conditions is not relevant."
+        },
+        {
+            "id": "SAF-4-safe",
+            "analyser": {
+                "eclair": "MC3R1.R13.1"
+            },
+            "name": "MC3R1.R13.1: volatile asm statements that do not perform any persistent side effect",
+            "text": "Volatile asm statement in an initializer list that does not perform persistent side effects is safe."
+        },
+        {
+            "id": "SAF-5-safe",
             "analyser": {},
             "name": "Sentinel",
             "text": "Next ID to be used"
diff --git a/xen/arch/arm/device.c b/xen/arch/arm/device.c
index 1f631d3274..fa331f164d 100644
--- a/xen/arch/arm/device.c
+++ b/xen/arch/arm/device.c
@@ -331,6 +331,7 @@ int handle_device(struct domain *d, struct dt_device_node *dev, p2m_type_t p2mt,
         .p2mt = p2mt,
         .skip_mapping = !own_device ||
                         (is_pci_passthrough_enabled() &&
+                        /* SAF-3-safe effects for debugging/logging reasons are safe */
                         (device_get_class(dev) == DEVICE_PCI_HOSTBRIDGE)),
         .iomem_ranges = iomem_ranges,
         .irq_ranges = irq_ranges
diff --git a/xen/arch/arm/guestcopy.c b/xen/arch/arm/guestcopy.c
index 6716b03561..b75538252a 100644
--- a/xen/arch/arm/guestcopy.c
+++ b/xen/arch/arm/guestcopy.c
@@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
 unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
 {
     return copy_guest((void *)from, (vaddr_t)to, len,
-                      GVA_INFO(current), COPY_to_guest | COPY_linear);
+                      /* SAF-4-safe No persistent side effects */
+                      GVA_INFO(current),
+                      COPY_to_guest | COPY_linear);
 }
 
 unsigned long raw_copy_to_guest_flush_dcache(void *to, const void *from,
                                              unsigned int len)
 {
-    return copy_guest((void *)from, (vaddr_t)to, len, GVA_INFO(current),
+    return copy_guest((void *)from, (vaddr_t)to, len,
+                      /* SAF-4-safe No persistent side effects */
+                      GVA_INFO(current),
                       COPY_to_guest | COPY_flush_dcache | COPY_linear);
 }
 
 unsigned long raw_clear_guest(void *to, unsigned int len)
 {
-    return copy_guest(NULL, (vaddr_t)to, len, GVA_INFO(current),
+    return copy_guest(NULL, (vaddr_t)to, len,
+                      /* SAF-4-safe No persistent side effects */
+                      GVA_INFO(current),
                       COPY_to_guest | COPY_linear);
 }
 
 unsigned long raw_copy_from_guest(void *to, const void __user *from,
                                   unsigned int len)
 {
-    return copy_guest(to, (vaddr_t)from, len, GVA_INFO(current),
+    return copy_guest(to, (vaddr_t)from, len,
+                      /* SAF-4-safe No persistent side effects */
+                      GVA_INFO(current),
                       COPY_from_guest | COPY_linear);
 }
 
diff --git a/xen/arch/x86/hvm/hvm.c b/xen/arch/x86/hvm/hvm.c
index e8deeb0222..19322fbb56 100644
--- a/xen/arch/x86/hvm/hvm.c
+++ b/xen/arch/x86/hvm/hvm.c
@@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu *v, hvm_domain_context_t *h)
 {
     struct segment_register seg;
     struct hvm_hw_cpu ctxt = {
+        /* SAF-3-safe effects for debugging/logging reasons are safe */
         .tsc = hvm_get_guest_tsc_fixed(v, v->domain->arch.hvm.sync_tsc),
         .msr_tsc_aux = v->arch.msrs->tsc_aux,
         .rax = v->arch.user_regs.rax,
diff --git a/xen/common/sched/core.c b/xen/common/sched/core.c
index d177c675c8..9e973fcf31 100644
--- a/xen/common/sched/core.c
+++ b/xen/common/sched/core.c
@@ -1521,6 +1521,7 @@ long vcpu_yield(void)
 
     SCHED_STAT_CRANK(vcpu_yield);
 
+    /* SAF-4-safe No persistent side effects */
     TRACE_2D(TRC_SCHED_YIELD, current->domain->domain_id, current->vcpu_id);
     raise_softirq(SCHEDULE_SOFTIRQ);
     return 0;
@@ -1899,6 +1900,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
         if ( copy_from_guest(&sched_shutdown, arg, 1) )
             break;
 
+        /* SAF-4-safe No persistent side effects */
         TRACE_3D(TRC_SCHED_SHUTDOWN,
                  current->domain->domain_id, current->vcpu_id,
                  sched_shutdown.reason);
@@ -1916,6 +1918,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
         if ( copy_from_guest(&sched_shutdown, arg, 1) )
             break;
 
+        /* SAF-4-safe No persistent side effects */
         TRACE_3D(TRC_SCHED_SHUTDOWN_CODE,
                  d->domain_id, current->vcpu_id, sched_shutdown.reason);
 
-- 
2.34.1

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Jan Beulich]

On 02.02.2024 16:16, Simone Ballarin wrote:
> Rule 13.1: Initializer lists shall not contain persistent side effects
> 
> Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
> LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
> lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
> of logging effects is always safe.

I thought I said so before: When talking of just logging, evaluation order
may very well have a impact on correctness. Therefore we shouldn't mix
debugging and logging.

> Function hvm_get_guest_tsc_fixed (indirectly) performs different side effects.
> For example it calls hvm_get_guest_time_fixed that contains an ASSERT and calls
> to spin_lock and spin_unlock.
> 
> These side effects are not dangerous: they can be executed regardless of the
> initializer list evaluation order
> 
> This patch deviates violations using SAF commits caused by debug/logging macros and
> functions.

DYM "comments"?

> --- a/xen/arch/arm/device.c
> +++ b/xen/arch/arm/device.c
> @@ -331,6 +331,7 @@ int handle_device(struct domain *d, struct dt_device_node *dev, p2m_type_t p2mt,
>          .p2mt = p2mt,
>          .skip_mapping = !own_device ||
>                          (is_pci_passthrough_enabled() &&
> +                        /* SAF-3-safe effects for debugging/logging reasons are safe */
>                          (device_get_class(dev) == DEVICE_PCI_HOSTBRIDGE)),

Taking this just as example: I think the comment is too long. Just
saying (leaving aside my comment higher up) "debugging/logging"
would imo be sufficient.

> --- a/xen/arch/arm/guestcopy.c
> +++ b/xen/arch/arm/guestcopy.c
> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>  unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>  {
>      return copy_guest((void *)from, (vaddr_t)to, len,
> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
> +                      /* SAF-4-safe No persistent side effects */
> +                      GVA_INFO(current),

I _still_ think this leaves ambiguity. The more that you need to look
up GVA_INFO() to recognize what this is about.

> --- a/xen/arch/x86/hvm/hvm.c
> +++ b/xen/arch/x86/hvm/hvm.c
> @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu *v, hvm_domain_context_t *h)
>  {
>      struct segment_register seg;
>      struct hvm_hw_cpu ctxt = {
> +        /* SAF-3-safe effects for debugging/logging reasons are safe */
>          .tsc = hvm_get_guest_tsc_fixed(v, v->domain->arch.hvm.sync_tsc),

A prereq for this imo is that the function take const struct vcpu *.
But I'm not sure that'll suffice. The function can change at any time,
rendering the comment here stale perhaps without anyone noticing.

> --- a/xen/common/sched/core.c
> +++ b/xen/common/sched/core.c
> @@ -1521,6 +1521,7 @@ long vcpu_yield(void)
>  
>      SCHED_STAT_CRANK(vcpu_yield);
>  
> +    /* SAF-4-safe No persistent side effects */
>      TRACE_2D(TRC_SCHED_YIELD, current->domain->domain_id, current->vcpu_id);
>      raise_softirq(SCHEDULE_SOFTIRQ);
>      return 0;
> @@ -1899,6 +1900,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
>          if ( copy_from_guest(&sched_shutdown, arg, 1) )
>              break;
>  
> +        /* SAF-4-safe No persistent side effects */
>          TRACE_3D(TRC_SCHED_SHUTDOWN,
>                   current->domain->domain_id, current->vcpu_id,
>                   sched_shutdown.reason);
> @@ -1916,6 +1918,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
>          if ( copy_from_guest(&sched_shutdown, arg, 1) )
>              break;
>  
> +        /* SAF-4-safe No persistent side effects */
>          TRACE_3D(TRC_SCHED_SHUTDOWN_CODE,
>                   d->domain_id, current->vcpu_id, sched_shutdown.reason);
>  

For all of these iirc the suggestion was to latch current into a local
variable (named "curr" by convention).

Jan

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Simone Ballarin]

On 06/02/24 13:04, Jan Beulich wrote:
> On 02.02.2024 16:16, Simone Ballarin wrote:
>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>
>> Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
>> LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
>> lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
>> of logging effects is always safe.
> 
> I thought I said so before: When talking of just logging, evaluation order
> may very well have a impact on correctness. Therefore we shouldn't mix
> debugging and logging.

My general feeling was that changes like the following one are not supported by
the community:

- x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
+ int field1 = function_with_logs_effects();
+ x = { .field1 = field1 /*other eventual code*/};

so I tried to deviate as much as possible.

If having log effects is a good reason to do changes like the above, I can
propose a patch in that sense.

> 
>> Function hvm_get_guest_tsc_fixed (indirectly) performs different side effects.
>> For example it calls hvm_get_guest_time_fixed that contains an ASSERT and calls
>> to spin_lock and spin_unlock.
>>
>> These side effects are not dangerous: they can be executed regardless of the
>> initializer list evaluation order
>>
>> This patch deviates violations using SAF commits caused by debug/logging macros and
>> functions.
> 
> DYM "comments"?
> 

Oh yes, sorry.

>> --- a/xen/arch/arm/device.c
>> +++ b/xen/arch/arm/device.c
>> @@ -331,6 +331,7 @@ int handle_device(struct domain *d, struct dt_device_node *dev, p2m_type_t p2mt,
>>           .p2mt = p2mt,
>>           .skip_mapping = !own_device ||
>>                           (is_pci_passthrough_enabled() &&
>> +                        /* SAF-3-safe effects for debugging/logging reasons are safe */
>>                           (device_get_class(dev) == DEVICE_PCI_HOSTBRIDGE)),
> 
> Taking this just as example: I think the comment is too long. Just
> saying (leaving aside my comment higher up) "debugging/logging"
> would imo be sufficient.
> 

Ok.

>> --- a/xen/arch/arm/guestcopy.c
>> +++ b/xen/arch/arm/guestcopy.c
>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>>   unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>>   {
>>       return copy_guest((void *)from, (vaddr_t)to, len,
>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
>> +                      /* SAF-4-safe No persistent side effects */
>> +                      GVA_INFO(current),
> 
> I _still_ think this leaves ambiguity. The more that you need to look
> up GVA_INFO() to recognize what this is about.


Just to recap: here the point is that current reads a register with a volatile asm, so the
violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
are completely fine, so this is the only place where a SAF comment can be placed.

The exapansion is:
((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
   per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
   (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));

My proposals are:
1) address the violation moving the current expansion outside (extra variable);
2) put a more detailed comment to avoid the ambiguity;
3) use an ECL deviation for GVA_INFO(current).

Do you have any preference or proposal?

>> --- a/xen/arch/x86/hvm/hvm.c
>> +++ b/xen/arch/x86/hvm/hvm.c
>> @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu *v, hvm_domain_context_t *h)
>>   {
>>       struct segment_register seg;
>>       struct hvm_hw_cpu ctxt = {
>> +        /* SAF-3-safe effects for debugging/logging reasons are safe */
>>           .tsc = hvm_get_guest_tsc_fixed(v, v->domain->arch.hvm.sync_tsc),
> 
> A prereq for this imo is that the function take const struct vcpu *.
> But I'm not sure that'll suffice. The function can change at any time,
> rendering the comment here stale perhaps without anyone noticing.
>

IMO It isn't a strict prereq, but it would make everything more clear.

In any case, apart adding the const, I do not see other easy solutions.
Would you give me your ack if I change the function signature?

Another possible solutions would be documenting the function in the new
JSON file with a special attribute like only_debug_effect. Of course,
this still requires keeping the JSON up to date in case of changes.

>> --- a/xen/common/sched/core.c
>> +++ b/xen/common/sched/core.c
>> @@ -1521,6 +1521,7 @@ long vcpu_yield(void)
>>   
>>       SCHED_STAT_CRANK(vcpu_yield);
>>   
>> +    /* SAF-4-safe No persistent side effects */
>>       TRACE_2D(TRC_SCHED_YIELD, current->domain->domain_id, current->vcpu_id);
>>       raise_softirq(SCHEDULE_SOFTIRQ);
>>       return 0;
>> @@ -1899,6 +1900,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
>>           if ( copy_from_guest(&sched_shutdown, arg, 1) )
>>               break;
>>   
>> +        /* SAF-4-safe No persistent side effects */
>>           TRACE_3D(TRC_SCHED_SHUTDOWN,
>>                    current->domain->domain_id, current->vcpu_id,
>>                    sched_shutdown.reason);
>> @@ -1916,6 +1918,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
>>           if ( copy_from_guest(&sched_shutdown, arg, 1) )
>>               break;
>>   
>> +        /* SAF-4-safe No persistent side effects */
>>           TRACE_3D(TRC_SCHED_SHUTDOWN_CODE,
>>                    d->domain_id, current->vcpu_id, sched_shutdown.reason);
>>   
> 
> For all of these iirc the suggestion was to latch current into a local
> variable (named "curr" by convention).
> 

Ok.

> Jan

-- 
Simone Ballarin, M.Sc.

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

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Jan Beulich]

On 07.02.2024 11:03, Simone Ballarin wrote:
> On 06/02/24 13:04, Jan Beulich wrote:
>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>>
>>> Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
>>> LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
>>> lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
>>> of logging effects is always safe.
>>
>> I thought I said so before: When talking of just logging, evaluation order
>> may very well have a impact on correctness. Therefore we shouldn't mix
>> debugging and logging.
> 
> My general feeling was that changes like the following one are not supported by
> the community:
> 
> - x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
> + int field1 = function_with_logs_effects();
> + x = { .field1 = field1 /*other eventual code*/};
> 
> so I tried to deviate as much as possible.
> 
> If having log effects is a good reason to do changes like the above, I can
> propose a patch in that sense.

Just to avoid misunderstandings: I'm not advocating for changes like the
one you outline above. I simply consider the rule too strict: There's
nothing at risk when there's just a single operation with side effects
in an initializer. Even when there are multiple such operations, whether
there's anything at risk depends on whether any of the side effects
actually collide. In a number of cases the compiler would actually warn
(and thus, due to -Werror, the build would fail).

The primary purpose of my comment here was that we need to please
separate debugging from logging side effects.

>>> --- a/xen/arch/arm/guestcopy.c
>>> +++ b/xen/arch/arm/guestcopy.c
>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>>>   unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>>>   {
>>>       return copy_guest((void *)from, (vaddr_t)to, len,
>>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
>>> +                      /* SAF-4-safe No persistent side effects */
>>> +                      GVA_INFO(current),
>>
>> I _still_ think this leaves ambiguity. The more that you need to look
>> up GVA_INFO() to recognize what this is about.
> 
> 
> Just to recap: here the point is that current reads a register with a volatile asm, so the
> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
> are completely fine, so this is the only place where a SAF comment can be placed.
> 
> The exapansion is:
> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
>    per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
>    (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
> 
> My proposals are:
> 1) address the violation moving the current expansion outside (extra variable);
> 2) put a more detailed comment to avoid the ambiguity;
> 3) use an ECL deviation for GVA_INFO(current).
> 
> Do you have any preference or proposal?

Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
I still wouldn't like it (as matching a general pattern I try to avoid:
introducing local variables that are used just once and don't meaningfully
improve e.g. readability). Therefore out of what you list, 2 would remain.
But I'm not happy with a comment here either - as per above, there's
nothing that can go wrong here as long as there's only a single construct
with side effect(s).

>>> --- a/xen/arch/x86/hvm/hvm.c
>>> +++ b/xen/arch/x86/hvm/hvm.c
>>> @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu *v, hvm_domain_context_t *h)
>>>   {
>>>       struct segment_register seg;
>>>       struct hvm_hw_cpu ctxt = {
>>> +        /* SAF-3-safe effects for debugging/logging reasons are safe */
>>>           .tsc = hvm_get_guest_tsc_fixed(v, v->domain->arch.hvm.sync_tsc),
>>
>> A prereq for this imo is that the function take const struct vcpu *.
>> But I'm not sure that'll suffice. The function can change at any time,
>> rendering the comment here stale perhaps without anyone noticing.
>>
> 
> IMO It isn't a strict prereq, but it would make everything more clear.
> 
> In any case, apart adding the const, I do not see other easy solutions.
> Would you give me your ack if I change the function signature?

Well, as said: I'm not sure that'll suffice.

> Another possible solutions would be documenting the function in the new
> JSON file with a special attribute like only_debug_effect. Of course,
> this still requires keeping the JSON up to date in case of changes.

Exactly. So wouldn't really help.

In any event I'd like to ask that you consider splitting up this patch,
such that you won't need multiple acks for any of the parts. That'll
also allow focusing on one aspect at a time in reviews.

Jan

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Simone Ballarin]

On 07/02/24 11:24, Jan Beulich wrote:
> On 07.02.2024 11:03, Simone Ballarin wrote:
>> On 06/02/24 13:04, Jan Beulich wrote:
>>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>>>
>>>> Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
>>>> LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
>>>> lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
>>>> of logging effects is always safe.
>>>
>>> I thought I said so before: When talking of just logging, evaluation order
>>> may very well have a impact on correctness. Therefore we shouldn't mix
>>> debugging and logging.
>>
>> My general feeling was that changes like the following one are not supported by
>> the community:
>>
>> - x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
>> + int field1 = function_with_logs_effects();
>> + x = { .field1 = field1 /*other eventual code*/};
>>
>> so I tried to deviate as much as possible.
>>
>> If having log effects is a good reason to do changes like the above, I can
>> propose a patch in that sense.
> 
> Just to avoid misunderstandings: I'm not advocating for changes like the
> one you outline above. I simply consider the rule too strict: There's
> nothing at risk when there's just a single operation with side effects
> in an initializer.

I agree for the safe cases such as single item list initializers (independently
by the number of effect contained in io_apic_read).
In fact, I was about to propose in another patch to deviate cases like:

union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };

> Even when there are multiple such operations, whether
> there's anything at risk depends on whether any of the side effects
> actually collide. In a number of cases the compiler would actually warn
> (and thus, due to -Werror, the build would fail).
> 

I don't completely agree on that, this requires an in-depth comprehension
of the code especially when complex call chains are involved. Moreover
these deviations need to be maintained when one of the function involved changes.

> The primary purpose of my comment here was that we need to please
> separate debugging from logging side effects.
>

Ok, I will work in that sense.

>>>> --- a/xen/arch/arm/guestcopy.c
>>>> +++ b/xen/arch/arm/guestcopy.c
>>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>>>>    unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>>>>    {
>>>>        return copy_guest((void *)from, (vaddr_t)to, len,
>>>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
>>>> +                      /* SAF-4-safe No persistent side effects */
>>>> +                      GVA_INFO(current),
>>>
>>> I _still_ think this leaves ambiguity. The more that you need to look
>>> up GVA_INFO() to recognize what this is about.
>>
>>
>> Just to recap: here the point is that current reads a register with a volatile asm, so the
>> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
>> are completely fine, so this is the only place where a SAF comment can be placed.
>>
>> The exapansion is:
>> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
>>     per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
>>     (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
>>
>> My proposals are:
>> 1) address the violation moving the current expansion outside (extra variable);
>> 2) put a more detailed comment to avoid the ambiguity;
>> 3) use an ECL deviation for GVA_INFO(current).
>>
>> Do you have any preference or proposal?
> 
> Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
> I still wouldn't like it (as matching a general pattern I try to avoid:
> introducing local variables that are used just once and don't meaningfully
> improve e.g. readability). Therefore out of what you list, 2 would remain.
> But I'm not happy with a comment here either - as per above, there's
> nothing that can go wrong here as long as there's only a single construct
> with side effect(s).
>
So, would be changing the SAF in:
/* SAF-<new_id>-safe single item initializer */

OK for you?

>>>> --- a/xen/arch/x86/hvm/hvm.c
>>>> +++ b/xen/arch/x86/hvm/hvm.c
>>>> @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu *v, hvm_domain_context_t *h)
>>>>    {
>>>>        struct segment_register seg;
>>>>        struct hvm_hw_cpu ctxt = {
>>>> +        /* SAF-3-safe effects for debugging/logging reasons are safe */
>>>>            .tsc = hvm_get_guest_tsc_fixed(v, v->domain->arch.hvm.sync_tsc),
>>>
>>> A prereq for this imo is that the function take const struct vcpu *.
>>> But I'm not sure that'll suffice. The function can change at any time,
>>> rendering the comment here stale perhaps without anyone noticing.
>>>
>>
>> IMO It isn't a strict prereq, but it would make everything more clear.
>>
>> In any case, apart adding the const, I do not see other easy solutions.
>> Would you give me your ack if I change the function signature?
> 
> Well, as said: I'm not sure that'll suffice.
> 
>> Another possible solutions would be documenting the function in the new
>> JSON file with a special attribute like only_debug_effect. Of course,
>> this still requires keeping the JSON up to date in case of changes.
> 
> Exactly. So wouldn't really help.
> 
> In any event I'd like to ask that you consider splitting up this patch,
> such that you won't need multiple acks for any of the parts. That'll
> also allow focusing on one aspect at a time in reviews.
> 

Ok, but please consider that the JSON file has been precisely added to deal
with these cases (avoiding __attribute__). If we are scared to use it, it becomes
meaningless.

@Stefano maybe your opinion could help.

Another more complex option would be emulating __attribute__ (in general any property)
with a comment:

/* @attribute: [only_debug_effects]
int foo(void);

This solution implies that:
- we need a script to convert these comments in ECL configurations (the script should
   parse the entire codebase);
- regexes cannot be used (the JSON instead accepts regexes);
- to be coherent, all properties that actually lives in the JSON should be moved inside
   these comments. This means a lot of changes. A hybrid approach is also possible.

> Jan

-- 
Simone Ballarin, M.Sc.

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

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Jan Beulich]

On 07.02.2024 13:21, Simone Ballarin wrote:
> On 07/02/24 11:24, Jan Beulich wrote:
>> On 07.02.2024 11:03, Simone Ballarin wrote:
>>> On 06/02/24 13:04, Jan Beulich wrote:
>>>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>>>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>>>>
>>>>> Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
>>>>> LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
>>>>> lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
>>>>> of logging effects is always safe.
>>>>
>>>> I thought I said so before: When talking of just logging, evaluation order
>>>> may very well have a impact on correctness. Therefore we shouldn't mix
>>>> debugging and logging.
>>>
>>> My general feeling was that changes like the following one are not supported by
>>> the community:
>>>
>>> - x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
>>> + int field1 = function_with_logs_effects();
>>> + x = { .field1 = field1 /*other eventual code*/};
>>>
>>> so I tried to deviate as much as possible.
>>>
>>> If having log effects is a good reason to do changes like the above, I can
>>> propose a patch in that sense.
>>
>> Just to avoid misunderstandings: I'm not advocating for changes like the
>> one you outline above. I simply consider the rule too strict: There's
>> nothing at risk when there's just a single operation with side effects
>> in an initializer.
> 
> I agree for the safe cases such as single item list initializers (independently
> by the number of effect contained in io_apic_read).
> In fact, I was about to propose in another patch to deviate cases like:
> 
> union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
> union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
> 
>> Even when there are multiple such operations, whether
>> there's anything at risk depends on whether any of the side effects
>> actually collide. In a number of cases the compiler would actually warn
>> (and thus, due to -Werror, the build would fail).
>>
> 
> I don't completely agree on that, this requires an in-depth comprehension
> of the code especially when complex call chains are involved. Moreover
> these deviations need to be maintained when one of the function involved changes.

Right, and I didn't really mean multiple function calls here, but e.g.
multiple ++ or --.

>>>>> --- a/xen/arch/arm/guestcopy.c
>>>>> +++ b/xen/arch/arm/guestcopy.c
>>>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>>>>>    unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>>>>>    {
>>>>>        return copy_guest((void *)from, (vaddr_t)to, len,
>>>>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
>>>>> +                      /* SAF-4-safe No persistent side effects */
>>>>> +                      GVA_INFO(current),
>>>>
>>>> I _still_ think this leaves ambiguity. The more that you need to look
>>>> up GVA_INFO() to recognize what this is about.
>>>
>>>
>>> Just to recap: here the point is that current reads a register with a volatile asm, so the
>>> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
>>> are completely fine, so this is the only place where a SAF comment can be placed.
>>>
>>> The exapansion is:
>>> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
>>>     per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
>>>     (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
>>>
>>> My proposals are:
>>> 1) address the violation moving the current expansion outside (extra variable);
>>> 2) put a more detailed comment to avoid the ambiguity;
>>> 3) use an ECL deviation for GVA_INFO(current).
>>>
>>> Do you have any preference or proposal?
>>
>> Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
>> I still wouldn't like it (as matching a general pattern I try to avoid:
>> introducing local variables that are used just once and don't meaningfully
>> improve e.g. readability). Therefore out of what you list, 2 would remain.
>> But I'm not happy with a comment here either - as per above, there's
>> nothing that can go wrong here as long as there's only a single construct
>> with side effect(s).
>>
> So, would be changing the SAF in:
> /* SAF-<new_id>-safe single item initializer */
> 
> OK for you?

A comment, as said, is only the least bad of what you did enumerate. But
for this code in particular I'm not a maintainer anyway, so it's not me
you need to convince. I'm taking this only as an example for discussing
underlying aspects.

Jan

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Simone Ballarin]

On 07/02/24 13:40, Jan Beulich wrote:
> On 07.02.2024 13:21, Simone Ballarin wrote:
>> On 07/02/24 11:24, Jan Beulich wrote:
>>> On 07.02.2024 11:03, Simone Ballarin wrote:
>>>> On 06/02/24 13:04, Jan Beulich wrote:
>>>>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>>>>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>>>>>
>>>>>> Effects caused by debug/logging macros and functions (like ASSERT, __bad_atomic_size,
>>>>>> LOG, etc ...) that crash execution or produce logs are not dangerous in initializer
>>>>>> lists. The evaluation order in abnormal conditions is not relevant. Evaluation order
>>>>>> of logging effects is always safe.
>>>>>
>>>>> I thought I said so before: When talking of just logging, evaluation order
>>>>> may very well have a impact on correctness. Therefore we shouldn't mix
>>>>> debugging and logging.
>>>>
>>>> My general feeling was that changes like the following one are not supported by
>>>> the community:
>>>>
>>>> - x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
>>>> + int field1 = function_with_logs_effects();
>>>> + x = { .field1 = field1 /*other eventual code*/};
>>>>
>>>> so I tried to deviate as much as possible.
>>>>
>>>> If having log effects is a good reason to do changes like the above, I can
>>>> propose a patch in that sense.
>>>
>>> Just to avoid misunderstandings: I'm not advocating for changes like the
>>> one you outline above. I simply consider the rule too strict: There's
>>> nothing at risk when there's just a single operation with side effects
>>> in an initializer.
>>
>> I agree for the safe cases such as single item list initializers (independently
>> by the number of effect contained in io_apic_read).
>> In fact, I was about to propose in another patch to deviate cases like:
>>
>> union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
>> union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
>>
>>> Even when there are multiple such operations, whether
>>> there's anything at risk depends on whether any of the side effects
>>> actually collide. In a number of cases the compiler would actually warn
>>> (and thus, due to -Werror, the build would fail).
>>>
>>
>> I don't completely agree on that, this requires an in-depth comprehension
>> of the code especially when complex call chains are involved. Moreover
>> these deviations need to be maintained when one of the function involved changes.
> 
> Right, and I didn't really mean multiple function calls here, but e.g.
> multiple ++ or --.
> 
>>>>>> --- a/xen/arch/arm/guestcopy.c
>>>>>> +++ b/xen/arch/arm/guestcopy.c
>>>>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>>>>>>     unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>>>>>>     {
>>>>>>         return copy_guest((void *)from, (vaddr_t)to, len,
>>>>>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
>>>>>> +                      /* SAF-4-safe No persistent side effects */
>>>>>> +                      GVA_INFO(current),
>>>>>
>>>>> I _still_ think this leaves ambiguity. The more that you need to look
>>>>> up GVA_INFO() to recognize what this is about.
>>>>
>>>>
>>>> Just to recap: here the point is that current reads a register with a volatile asm, so the
>>>> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
>>>> are completely fine, so this is the only place where a SAF comment can be placed.
>>>>
>>>> The exapansion is:
>>>> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
>>>>      per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
>>>>      (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
>>>>
>>>> My proposals are:
>>>> 1) address the violation moving the current expansion outside (extra variable);
>>>> 2) put a more detailed comment to avoid the ambiguity;
>>>> 3) use an ECL deviation for GVA_INFO(current).
>>>>
>>>> Do you have any preference or proposal?
>>>
>>> Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
>>> I still wouldn't like it (as matching a general pattern I try to avoid:
>>> introducing local variables that are used just once and don't meaningfully
>>> improve e.g. readability). Therefore out of what you list, 2 would remain.
>>> But I'm not happy with a comment here either - as per above, there's
>>> nothing that can go wrong here as long as there's only a single construct
>>> with side effect(s).
>>>
>> So, would be changing the SAF in:
>> /* SAF-<new_id>-safe single item initializer */
>>
>> OK for you?
> 
> A comment, as said, is only the least bad of what you did enumerate. But
> for this code in particular I'm not a maintainer anyway, so it's not me
> you need to convince. I'm taking this only as an example for discussing
> underlying aspects.
> 
> Jan
> 

I was generally thinking about the comments of this series, and I've
just realised that many of them can be summarized by the following sentence:

"We do not want changes to address violations of R13.1 that are not also violations
of R13.2"

MC3R1.R13.2	rule	The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders
MC3R1.R13.1	rule	Initializer lists shall not contain persistent side effects

At this point, my proposal is to remove R13.1 from the coding standard and add
R13.2 (eventually limiting its scope to initializer lists).
Maybe it is better to re-discuss the rule adoption during the next meeting?


-- 
Simone Ballarin, M.Sc.

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

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Jan Beulich]

On 09.02.2024 10:25, Simone Ballarin wrote:
> On 07/02/24 13:40, Jan Beulich wrote:
>> On 07.02.2024 13:21, Simone Ballarin wrote:
>>> On 07/02/24 11:24, Jan Beulich wrote:
>>>> On 07.02.2024 11:03, Simone Ballarin wrote:
>>>>> On 06/02/24 13:04, Jan Beulich wrote:
>>>>>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>>>>>> --- a/xen/arch/arm/guestcopy.c
>>>>>>> +++ b/xen/arch/arm/guestcopy.c
>>>>>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
>>>>>>>     unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
>>>>>>>     {
>>>>>>>         return copy_guest((void *)from, (vaddr_t)to, len,
>>>>>>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
>>>>>>> +                      /* SAF-4-safe No persistent side effects */
>>>>>>> +                      GVA_INFO(current),
>>>>>>
>>>>>> I _still_ think this leaves ambiguity. The more that you need to look
>>>>>> up GVA_INFO() to recognize what this is about.
>>>>>
>>>>>
>>>>> Just to recap: here the point is that current reads a register with a volatile asm, so the
>>>>> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
>>>>> are completely fine, so this is the only place where a SAF comment can be placed.
>>>>>
>>>>> The exapansion is:
>>>>> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
>>>>>      per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
>>>>>      (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
>>>>>
>>>>> My proposals are:
>>>>> 1) address the violation moving the current expansion outside (extra variable);
>>>>> 2) put a more detailed comment to avoid the ambiguity;
>>>>> 3) use an ECL deviation for GVA_INFO(current).
>>>>>
>>>>> Do you have any preference or proposal?
>>>>
>>>> Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
>>>> I still wouldn't like it (as matching a general pattern I try to avoid:
>>>> introducing local variables that are used just once and don't meaningfully
>>>> improve e.g. readability). Therefore out of what you list, 2 would remain.
>>>> But I'm not happy with a comment here either - as per above, there's
>>>> nothing that can go wrong here as long as there's only a single construct
>>>> with side effect(s).
>>>>
>>> So, would be changing the SAF in:
>>> /* SAF-<new_id>-safe single item initializer */
>>>
>>> OK for you?
>>
>> A comment, as said, is only the least bad of what you did enumerate. But
>> for this code in particular I'm not a maintainer anyway, so it's not me
>> you need to convince. I'm taking this only as an example for discussing
>> underlying aspects.
> 
> I was generally thinking about the comments of this series, and I've
> just realised that many of them can be summarized by the following sentence:
> 
> "We do not want changes to address violations of R13.1 that are not also violations
> of R13.2"
> 
> MC3R1.R13.2	rule	The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders
> MC3R1.R13.1	rule	Initializer lists shall not contain persistent side effects
> 
> At this point, my proposal is to remove R13.1 from the coding standard and add
> R13.2 (eventually limiting its scope to initializer lists).

I'm afraid I don't understand the "eventually limiting" part.

> Maybe it is better to re-discuss the rule adoption during the next meeting?

Perhaps best. Stefano, could you take note of this?

Jan

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Stefano Stabellini]

On Fri, 9 Feb 2024, Jan Beulich wrote:
> On 09.02.2024 10:25, Simone Ballarin wrote:
> > On 07/02/24 13:40, Jan Beulich wrote:
> >> On 07.02.2024 13:21, Simone Ballarin wrote:
> >>> On 07/02/24 11:24, Jan Beulich wrote:
> >>>> On 07.02.2024 11:03, Simone Ballarin wrote:
> >>>>> On 06/02/24 13:04, Jan Beulich wrote:
> >>>>>> On 02.02.2024 16:16, Simone Ballarin wrote:
> >>>>>>> --- a/xen/arch/arm/guestcopy.c
> >>>>>>> +++ b/xen/arch/arm/guestcopy.c
> >>>>>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t addr, unsigned int len,
> >>>>>>>     unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int len)
> >>>>>>>     {
> >>>>>>>         return copy_guest((void *)from, (vaddr_t)to, len,
> >>>>>>> -                      GVA_INFO(current), COPY_to_guest | COPY_linear);
> >>>>>>> +                      /* SAF-4-safe No persistent side effects */
> >>>>>>> +                      GVA_INFO(current),
> >>>>>>
> >>>>>> I _still_ think this leaves ambiguity. The more that you need to look
> >>>>>> up GVA_INFO() to recognize what this is about.
> >>>>>
> >>>>>
> >>>>> Just to recap: here the point is that current reads a register with a volatile asm, so the
> >>>>> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and current taken alone
> >>>>> are completely fine, so this is the only place where a SAF comment can be placed.
> >>>>>
> >>>>> The exapansion is:
> >>>>> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" : "=r"(__ptr) : "0"(&
> >>>>>      per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({ uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
> >>>>>      (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
> >>>>>
> >>>>> My proposals are:
> >>>>> 1) address the violation moving the current expansion outside (extra variable);
> >>>>> 2) put a more detailed comment to avoid the ambiguity;
> >>>>> 3) use an ECL deviation for GVA_INFO(current).
> >>>>>
> >>>>> Do you have any preference or proposal?
> >>>>
> >>>> Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
> >>>> I still wouldn't like it (as matching a general pattern I try to avoid:
> >>>> introducing local variables that are used just once and don't meaningfully
> >>>> improve e.g. readability). Therefore out of what you list, 2 would remain.
> >>>> But I'm not happy with a comment here either - as per above, there's
> >>>> nothing that can go wrong here as long as there's only a single construct
> >>>> with side effect(s).
> >>>>
> >>> So, would be changing the SAF in:
> >>> /* SAF-<new_id>-safe single item initializer */
> >>>
> >>> OK for you?
> >>
> >> A comment, as said, is only the least bad of what you did enumerate. But
> >> for this code in particular I'm not a maintainer anyway, so it's not me
> >> you need to convince. I'm taking this only as an example for discussing
> >> underlying aspects.
> > 
> > I was generally thinking about the comments of this series, and I've
> > just realised that many of them can be summarized by the following sentence:
> > 
> > "We do not want changes to address violations of R13.1 that are not also violations
> > of R13.2"
> > 
> > MC3R1.R13.2	rule	The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders
> > MC3R1.R13.1	rule	Initializer lists shall not contain persistent side effects
> > 
> > At this point, my proposal is to remove R13.1 from the coding standard and add
> > R13.2 (eventually limiting its scope to initializer lists).
> 
> I'm afraid I don't understand the "eventually limiting" part.
> 
> > Maybe it is better to re-discuss the rule adoption during the next meeting?
> 
> Perhaps best. Stefano, could you take note of this?

Yes. I think Simone might be right: it looks like the cases we care
about the most are the ones covered by 13.2, which appear to be a subset
of the ones covered by 13.1.

Assuming we accept 13.2, the question is whether there is anything left
in 13.1 that is of interest. We can discuss during the next MISRA call.

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Stefano Stabellini]

On Wed, 7 Feb 2024, Simone Ballarin wrote:
> On 07/02/24 11:24, Jan Beulich wrote:
> > On 07.02.2024 11:03, Simone Ballarin wrote:
> > > On 06/02/24 13:04, Jan Beulich wrote:
> > > > On 02.02.2024 16:16, Simone Ballarin wrote:
> > > > > Rule 13.1: Initializer lists shall not contain persistent side effects
> > > > > 
> > > > > Effects caused by debug/logging macros and functions (like ASSERT,
> > > > > __bad_atomic_size,
> > > > > LOG, etc ...) that crash execution or produce logs are not dangerous
> > > > > in initializer
> > > > > lists. The evaluation order in abnormal conditions is not relevant.
> > > > > Evaluation order
> > > > > of logging effects is always safe.
> > > > 
> > > > I thought I said so before: When talking of just logging, evaluation
> > > > order
> > > > may very well have a impact on correctness. Therefore we shouldn't mix
> > > > debugging and logging.
> > > 
> > > My general feeling was that changes like the following one are not
> > > supported by
> > > the community:
> > > 
> > > - x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
> > > + int field1 = function_with_logs_effects();
> > > + x = { .field1 = field1 /*other eventual code*/};
> > > 
> > > so I tried to deviate as much as possible.
> > > 
> > > If having log effects is a good reason to do changes like the above, I can
> > > propose a patch in that sense.
> > 
> > Just to avoid misunderstandings: I'm not advocating for changes like the
> > one you outline above. I simply consider the rule too strict: There's
> > nothing at risk when there's just a single operation with side effects
> > in an initializer.
> 
> I agree for the safe cases such as single item list initializers
> (independently
> by the number of effect contained in io_apic_read).
> In fact, I was about to propose in another patch to deviate cases like:
> 
> union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
> union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
> 
> > Even when there are multiple such operations, whether
> > there's anything at risk depends on whether any of the side effects
> > actually collide. In a number of cases the compiler would actually warn
> > (and thus, due to -Werror, the build would fail).
> > 
> 
> I don't completely agree on that, this requires an in-depth comprehension
> of the code especially when complex call chains are involved. Moreover
> these deviations need to be maintained when one of the function involved
> changes.
> 
> > The primary purpose of my comment here was that we need to please
> > separate debugging from logging side effects.
> > 
> 
> Ok, I will work in that sense.
> 
> > > > > --- a/xen/arch/arm/guestcopy.c
> > > > > +++ b/xen/arch/arm/guestcopy.c
> > > > > @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf,
> > > > > uint64_t addr, unsigned int len,
> > > > >    unsigned long raw_copy_to_guest(void *to, const void *from,
> > > > > unsigned int len)
> > > > >    {
> > > > >        return copy_guest((void *)from, (vaddr_t)to, len,
> > > > > -                      GVA_INFO(current), COPY_to_guest |
> > > > > COPY_linear);
> > > > > +                      /* SAF-4-safe No persistent side effects */
> > > > > +                      GVA_INFO(current),
> > > > 
> > > > I _still_ think this leaves ambiguity. The more that you need to look
> > > > up GVA_INFO() to recognize what this is about.
> > > 
> > > 
> > > Just to recap: here the point is that current reads a register with a
> > > volatile asm, so the
> > > violation is in the expansion of GVA_INFO(current). Both GVA_INFO and
> > > current taken alone
> > > are completely fine, so this is the only place where a SAF comment can be
> > > placed.
> > > 
> > > The exapansion is:
> > > ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" :
> > > "=r"(__ptr) : "0"(&
> > >     per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({
> > > uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
> > >     (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
> > > 
> > > My proposals are:
> > > 1) address the violation moving the current expansion outside (extra
> > > variable);
> > > 2) put a more detailed comment to avoid the ambiguity;
> > > 3) use an ECL deviation for GVA_INFO(current).
> > > 
> > > Do you have any preference or proposal?
> > 
> > Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
> > I still wouldn't like it (as matching a general pattern I try to avoid:
> > introducing local variables that are used just once and don't meaningfully
> > improve e.g. readability). Therefore out of what you list, 2 would remain.
> > But I'm not happy with a comment here either - as per above, there's
> > nothing that can go wrong here as long as there's only a single construct
> > with side effect(s).
> > 
> So, would be changing the SAF in:
> /* SAF-<new_id>-safe single item initializer */
> 
> OK for you?
> 
> > > > > --- a/xen/arch/x86/hvm/hvm.c
> > > > > +++ b/xen/arch/x86/hvm/hvm.c
> > > > > @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu
> > > > > *v, hvm_domain_context_t *h)
> > > > >    {
> > > > >        struct segment_register seg;
> > > > >        struct hvm_hw_cpu ctxt = {
> > > > > +        /* SAF-3-safe effects for debugging/logging reasons are safe
> > > > > */
> > > > >            .tsc = hvm_get_guest_tsc_fixed(v,
> > > > > v->domain->arch.hvm.sync_tsc),
> > > > 
> > > > A prereq for this imo is that the function take const struct vcpu *.
> > > > But I'm not sure that'll suffice. The function can change at any time,
> > > > rendering the comment here stale perhaps without anyone noticing.
> > > > 
> > > 
> > > IMO It isn't a strict prereq, but it would make everything more clear.
> > > 
> > > In any case, apart adding the const, I do not see other easy solutions.
> > > Would you give me your ack if I change the function signature?
> > 
> > Well, as said: I'm not sure that'll suffice.
> > 
> > > Another possible solutions would be documenting the function in the new
> > > JSON file with a special attribute like only_debug_effect. Of course,
> > > this still requires keeping the JSON up to date in case of changes.
> > 
> > Exactly. So wouldn't really help.
> > 
> > In any event I'd like to ask that you consider splitting up this patch,
> > such that you won't need multiple acks for any of the parts. That'll
> > also allow focusing on one aspect at a time in reviews.
> > 
> 
> Ok, but please consider that the JSON file has been precisely added to deal
> with these cases (avoiding __attribute__). If we are scared to use it, it
> becomes
> meaningless.
> 
> @Stefano maybe your opinion could help.

I do think the JSON file is a useful tool in our toolbox. It is also
fair to say that it is one that we should be careful about using as it
requires manual updates from time to time.

So, I certainly consider it an option, but I prefer your other
suggestion of dropping 13.1 in favor of 13.2. With that change, would
the need for a deviation in this function go away?

Re: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects

[Simone Ballarin]

On 09/02/24 23:13, Stefano Stabellini wrote:
> On Wed, 7 Feb 2024, Simone Ballarin wrote:
>> On 07/02/24 11:24, Jan Beulich wrote:
>>> On 07.02.2024 11:03, Simone Ballarin wrote:
>>>> On 06/02/24 13:04, Jan Beulich wrote:
>>>>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>>>>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>>>>>
>>>>>> Effects caused by debug/logging macros and functions (like ASSERT,
>>>>>> __bad_atomic_size,
>>>>>> LOG, etc ...) that crash execution or produce logs are not dangerous
>>>>>> in initializer
>>>>>> lists. The evaluation order in abnormal conditions is not relevant.
>>>>>> Evaluation order
>>>>>> of logging effects is always safe.
>>>>>
>>>>> I thought I said so before: When talking of just logging, evaluation
>>>>> order
>>>>> may very well have a impact on correctness. Therefore we shouldn't mix
>>>>> debugging and logging.
>>>>
>>>> My general feeling was that changes like the following one are not
>>>> supported by
>>>> the community:
>>>>
>>>> - x = { .field1 = function_with_logs_effects() /*other eventual code*/ };
>>>> + int field1 = function_with_logs_effects();
>>>> + x = { .field1 = field1 /*other eventual code*/};
>>>>
>>>> so I tried to deviate as much as possible.
>>>>
>>>> If having log effects is a good reason to do changes like the above, I can
>>>> propose a patch in that sense.
>>>
>>> Just to avoid misunderstandings: I'm not advocating for changes like the
>>> one you outline above. I simply consider the rule too strict: There's
>>> nothing at risk when there's just a single operation with side effects
>>> in an initializer.
>>
>> I agree for the safe cases such as single item list initializers
>> (independently
>> by the number of effect contained in io_apic_read).
>> In fact, I was about to propose in another patch to deviate cases like:
>>
>> union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
>> union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
>>
>>> Even when there are multiple such operations, whether
>>> there's anything at risk depends on whether any of the side effects
>>> actually collide. In a number of cases the compiler would actually warn
>>> (and thus, due to -Werror, the build would fail).
>>>
>>
>> I don't completely agree on that, this requires an in-depth comprehension
>> of the code especially when complex call chains are involved. Moreover
>> these deviations need to be maintained when one of the function involved
>> changes.
>>
>>> The primary purpose of my comment here was that we need to please
>>> separate debugging from logging side effects.
>>>
>>
>> Ok, I will work in that sense.
>>
>>>>>> --- a/xen/arch/arm/guestcopy.c
>>>>>> +++ b/xen/arch/arm/guestcopy.c
>>>>>> @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf,
>>>>>> uint64_t addr, unsigned int len,
>>>>>>     unsigned long raw_copy_to_guest(void *to, const void *from,
>>>>>> unsigned int len)
>>>>>>     {
>>>>>>         return copy_guest((void *)from, (vaddr_t)to, len,
>>>>>> -                      GVA_INFO(current), COPY_to_guest |
>>>>>> COPY_linear);
>>>>>> +                      /* SAF-4-safe No persistent side effects */
>>>>>> +                      GVA_INFO(current),
>>>>>
>>>>> I _still_ think this leaves ambiguity. The more that you need to look
>>>>> up GVA_INFO() to recognize what this is about.
>>>>
>>>>
>>>> Just to recap: here the point is that current reads a register with a
>>>> volatile asm, so the
>>>> violation is in the expansion of GVA_INFO(current). Both GVA_INFO and
>>>> current taken alone
>>>> are completely fine, so this is the only place where a SAF comment can be
>>>> placed.
>>>>
>>>> The exapansion is:
>>>> ((copy_info_t) { .gva = { ((*({ unsigned long __ptr; __asm__ ("" :
>>>> "=r"(__ptr) : "0"(&
>>>>      per_cpu__curr_vcpu)); (typeof(&per_cpu__curr_vcpu)) (__ptr + (({
>>>> uint64_t _r; asm volatile("mrs  %0, ""TPIDR_EL2" : "=r"
>>>>      (_r)); _r; }))); }))) } }), (1U << 1) | (1U << 2));
>>>>
>>>> My proposals are:
>>>> 1) address the violation moving the current expansion outside (extra
>>>> variable);
>>>> 2) put a more detailed comment to avoid the ambiguity;
>>>> 3) use an ECL deviation for GVA_INFO(current).
>>>>
>>>> Do you have any preference or proposal?
>>>
>>> Imo 3 is not an option at all. Probably 1 wouldn't be too bad here, but
>>> I still wouldn't like it (as matching a general pattern I try to avoid:
>>> introducing local variables that are used just once and don't meaningfully
>>> improve e.g. readability). Therefore out of what you list, 2 would remain.
>>> But I'm not happy with a comment here either - as per above, there's
>>> nothing that can go wrong here as long as there's only a single construct
>>> with side effect(s).
>>>
>> So, would be changing the SAF in:
>> /* SAF-<new_id>-safe single item initializer */
>>
>> OK for you?
>>
>>>>>> --- a/xen/arch/x86/hvm/hvm.c
>>>>>> +++ b/xen/arch/x86/hvm/hvm.c
>>>>>> @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu
>>>>>> *v, hvm_domain_context_t *h)
>>>>>>     {
>>>>>>         struct segment_register seg;
>>>>>>         struct hvm_hw_cpu ctxt = {
>>>>>> +        /* SAF-3-safe effects for debugging/logging reasons are safe
>>>>>> */
>>>>>>             .tsc = hvm_get_guest_tsc_fixed(v,
>>>>>> v->domain->arch.hvm.sync_tsc),
>>>>>
>>>>> A prereq for this imo is that the function take const struct vcpu *.
>>>>> But I'm not sure that'll suffice. The function can change at any time,
>>>>> rendering the comment here stale perhaps without anyone noticing.
>>>>>
>>>>
>>>> IMO It isn't a strict prereq, but it would make everything more clear.
>>>>
>>>> In any case, apart adding the const, I do not see other easy solutions.
>>>> Would you give me your ack if I change the function signature?
>>>
>>> Well, as said: I'm not sure that'll suffice.
>>>
>>>> Another possible solutions would be documenting the function in the new
>>>> JSON file with a special attribute like only_debug_effect. Of course,
>>>> this still requires keeping the JSON up to date in case of changes.
>>>
>>> Exactly. So wouldn't really help.
>>>
>>> In any event I'd like to ask that you consider splitting up this patch,
>>> such that you won't need multiple acks for any of the parts. That'll
>>> also allow focusing on one aspect at a time in reviews.
>>>
>>
>> Ok, but please consider that the JSON file has been precisely added to deal
>> with these cases (avoiding __attribute__). If we are scared to use it, it
>> becomes
>> meaningless.
>>
>> @Stefano maybe your opinion could help.
> 
> I do think the JSON file is a useful tool in our toolbox. It is also
> fair to say that it is one that we should be careful about using as it
> requires manual updates from time to time.
> 
> So, I certainly consider it an option, but I prefer your other
> suggestion of dropping 13.1 in favor of 13.2. With that change, would
> the need for a deviation in this function go away?
> 

This is only a violation of 13.1, so dropping it in favour of 13.2 it's
enough.

-- 
Simone Ballarin, M.Sc.

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

[XEN PATCH v4 2/4] xen/ns16550: address violations of MISRA C:2012 Rule 13.1

[Simone Ballarin]

Rule 13.1: Initializer lists shall not contain persistent side effects

The assignment operation in:

.irq = rc = uart->irq,

is a persistent side effect in a struct initializer list.

This patch assigns rc separately outside the structure.

No functional change.

Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>

---
Changes in v3:
- add assignment of rc;
- use rc as controlling expression in the following if-statement;
- change prefix from xen to xen/ns16550.
Changes in v2:
- avoid assignment of rc;
- drop changes in vcpu_yield(void).
---
 xen/drivers/char/ns16550.c | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/xen/drivers/char/ns16550.c b/xen/drivers/char/ns16550.c
index afe3d514b9..97bf098534 100644
--- a/xen/drivers/char/ns16550.c
+++ b/xen/drivers/char/ns16550.c
@@ -441,10 +441,12 @@ static void __init cf_check ns16550_init_postirq(struct serial_port *port)
             struct msi_info msi = {
                 .sbdf = PCI_SBDF(0, uart->ps_bdf[0], uart->ps_bdf[1],
                                  uart->ps_bdf[2]),
-                .irq = rc = uart->irq,
+                .irq = uart->irq,
                 .entry_nr = 1
             };
 
+            rc = uart->irq;
+
             if ( rc > 0 )
             {
                 struct msi_desc *msi_desc = NULL;
-- 
2.34.1

Re: [XEN PATCH v4 2/4] xen/ns16550: address violations of MISRA C:2012 Rule 13.1

[Jan Beulich]

On 02.02.2024 16:16, Simone Ballarin wrote:
> Rule 13.1: Initializer lists shall not contain persistent side effects
> 
> The assignment operation in:
> 
> .irq = rc = uart->irq,
> 
> is a persistent side effect in a struct initializer list.
> 
> This patch assigns rc separately outside the structure.
> 
> No functional change.
> 
> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
> Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>

Acked-by: Jan Beulich <jbeulich@suse.com>

Nevertheless I think this would have benefited from limiting rc's
scope.

Jan

[XEN PATCH v4 3/4] xen/x86: address violations of MISRA C:2012 Rule 13.1

[Simone Ballarin]

Rule 13.1: Initializer lists shall not contain persistent side effects

This patch moves expressions with side-effects into new variables before
the initializer lists.

No functional changes.

Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
---
 xen/arch/x86/io_apic.c | 9 ++++++---
 xen/arch/x86/mpparse.c | 3 ++-
 xen/arch/x86/setup.c   | 3 ++-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/xen/arch/x86/io_apic.c b/xen/arch/x86/io_apic.c
index b48a642465..4a6ab85689 100644
--- a/xen/arch/x86/io_apic.c
+++ b/xen/arch/x86/io_apic.c
@@ -2559,9 +2559,12 @@ integer_param("max_gsi_irqs", max_gsi_irqs);
 
 static __init bool bad_ioapic_register(unsigned int idx)
 {
-    union IO_APIC_reg_00 reg_00 = { .raw = io_apic_read(idx, 0) };
-    union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
-    union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
+    uint32_t reg_00_raw = io_apic_read(idx, 0);
+    uint32_t reg_01_raw = io_apic_read(idx, 1);
+    uint32_t reg_02_raw = io_apic_read(idx, 2);
+    union IO_APIC_reg_00 reg_00 = { .raw = reg_00_raw };
+    union IO_APIC_reg_01 reg_01 = { .raw = reg_01_raw };
+    union IO_APIC_reg_02 reg_02 = { .raw = reg_02_raw };
 
     if ( reg_00.raw == -1 && reg_01.raw == -1 && reg_02.raw == -1 )
     {
diff --git a/xen/arch/x86/mpparse.c b/xen/arch/x86/mpparse.c
index d8ccab2449..81a819403b 100644
--- a/xen/arch/x86/mpparse.c
+++ b/xen/arch/x86/mpparse.c
@@ -798,11 +798,12 @@ void __init mp_register_lapic_address (
 
 int mp_register_lapic(u32 id, bool enabled, bool hotplug)
 {
+	u32 apic = apic_read(APIC_LVR);
 	struct mpc_config_processor processor = {
 		.mpc_type = MP_PROCESSOR,
 		/* Note: We don't fill in fields not consumed anywhere. */
 		.mpc_apicid = id,
-		.mpc_apicver = GET_APIC_VERSION(apic_read(APIC_LVR)),
+		.mpc_apicver = GET_APIC_VERSION(apic),
 		.mpc_cpuflag = (enabled ? CPU_ENABLED : 0) |
 			       (id == boot_cpu_physical_apicid ?
 				CPU_BOOTPROCESSOR : 0),
diff --git a/xen/arch/x86/setup.c b/xen/arch/x86/setup.c
index ee682dd136..886031d86a 100644
--- a/xen/arch/x86/setup.c
+++ b/xen/arch/x86/setup.c
@@ -885,13 +885,14 @@ static struct domain *__init create_dom0(const module_t *image,
 {
     static char __initdata cmdline[MAX_GUEST_CMDLINE];
 
+    unsigned int max_vcpus = dom0_max_vcpus();
     struct xen_domctl_createdomain dom0_cfg = {
         .flags = IS_ENABLED(CONFIG_TBOOT) ? XEN_DOMCTL_CDF_s3_integrity : 0,
         .max_evtchn_port = -1,
         .max_grant_frames = -1,
         .max_maptrack_frames = -1,
         .grant_opts = XEN_DOMCTL_GRANT_version(opt_gnttab_max_version),
-        .max_vcpus = dom0_max_vcpus(),
+        .max_vcpus = max_vcpus,
         .arch = {
             .misc_flags = opt_dom0_msr_relaxed ? XEN_X86_MSR_RELAXED : 0,
         },
-- 
2.34.1

Re: [XEN PATCH v4 3/4] xen/x86: address violations of MISRA C:2012 Rule 13.1

[Jan Beulich]

On 02.02.2024 16:16, Simone Ballarin wrote:
> Rule 13.1: Initializer lists shall not contain persistent side effects
> 
> This patch moves expressions with side-effects into new variables before
> the initializer lists.
> 
> No functional changes.
> 
> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>

To be honest, I don't like this. It's more code for no gain. Really its
hampering clarity imo. I'm willing to be convinced otherwise, but for
now this gets a nack from me.

As an aside, ...

> --- a/xen/arch/x86/io_apic.c
> +++ b/xen/arch/x86/io_apic.c
> @@ -2559,9 +2559,12 @@ integer_param("max_gsi_irqs", max_gsi_irqs);
>  
>  static __init bool bad_ioapic_register(unsigned int idx)
>  {
> -    union IO_APIC_reg_00 reg_00 = { .raw = io_apic_read(idx, 0) };
> -    union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
> -    union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
> +    uint32_t reg_00_raw = io_apic_read(idx, 0);
> +    uint32_t reg_01_raw = io_apic_read(idx, 1);
> +    uint32_t reg_02_raw = io_apic_read(idx, 2);

... while you properly use uint32_t here, ...

> +    union IO_APIC_reg_00 reg_00 = { .raw = reg_00_raw };
> +    union IO_APIC_reg_01 reg_01 = { .raw = reg_01_raw };
> +    union IO_APIC_reg_02 reg_02 = { .raw = reg_02_raw };
>  
>      if ( reg_00.raw == -1 && reg_01.raw == -1 && reg_02.raw == -1 )
>      {
> --- a/xen/arch/x86/mpparse.c
> +++ b/xen/arch/x86/mpparse.c
> @@ -798,11 +798,12 @@ void __init mp_register_lapic_address (
>  
>  int mp_register_lapic(u32 id, bool enabled, bool hotplug)
>  {
> +	u32 apic = apic_read(APIC_LVR);

... why the being-phased-out u32 here?

Jan

>  	struct mpc_config_processor processor = {
>  		.mpc_type = MP_PROCESSOR,
>  		/* Note: We don't fill in fields not consumed anywhere. */
>  		.mpc_apicid = id,
> -		.mpc_apicver = GET_APIC_VERSION(apic_read(APIC_LVR)),
> +		.mpc_apicver = GET_APIC_VERSION(apic),
>  		.mpc_cpuflag = (enabled ? CPU_ENABLED : 0) |
>  			       (id == boot_cpu_physical_apicid ?
>  				CPU_BOOTPROCESSOR : 0),
> --- a/xen/arch/x86/setup.c
> +++ b/xen/arch/x86/setup.c
> @@ -885,13 +885,14 @@ static struct domain *__init create_dom0(const module_t *image,
>  {
>      static char __initdata cmdline[MAX_GUEST_CMDLINE];
>  
> +    unsigned int max_vcpus = dom0_max_vcpus();
>      struct xen_domctl_createdomain dom0_cfg = {
>          .flags = IS_ENABLED(CONFIG_TBOOT) ? XEN_DOMCTL_CDF_s3_integrity : 0,
>          .max_evtchn_port = -1,
>          .max_grant_frames = -1,
>          .max_maptrack_frames = -1,
>          .grant_opts = XEN_DOMCTL_GRANT_version(opt_gnttab_max_version),
> -        .max_vcpus = dom0_max_vcpus(),
> +        .max_vcpus = max_vcpus,
>          .arch = {
>              .misc_flags = opt_dom0_msr_relaxed ? XEN_X86_MSR_RELAXED : 0,
>          },

Re: [XEN PATCH v4 3/4] xen/x86: address violations of MISRA C:2012 Rule 13.1

[Stefano Stabellini]

On Tue, 6 Feb 2024, Jan Beulich wrote:
> On 02.02.2024 16:16, Simone Ballarin wrote:
> > Rule 13.1: Initializer lists shall not contain persistent side effects
> > 
> > This patch moves expressions with side-effects into new variables before
> > the initializer lists.
> > 
> > No functional changes.
> > 
> > Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
> 
> To be honest, I don't like this. It's more code for no gain. Really its
> hampering clarity imo. I'm willing to be convinced otherwise, but for
> now this gets a nack from me.

Which part of the patch you don't like? The changes to
bad_ioapic_register?



> As an aside, ...
> 
> > --- a/xen/arch/x86/io_apic.c
> > +++ b/xen/arch/x86/io_apic.c
> > @@ -2559,9 +2559,12 @@ integer_param("max_gsi_irqs", max_gsi_irqs);
> >  
> >  static __init bool bad_ioapic_register(unsigned int idx)
> >  {
> > -    union IO_APIC_reg_00 reg_00 = { .raw = io_apic_read(idx, 0) };
> > -    union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
> > -    union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
> > +    uint32_t reg_00_raw = io_apic_read(idx, 0);
> > +    uint32_t reg_01_raw = io_apic_read(idx, 1);
> > +    uint32_t reg_02_raw = io_apic_read(idx, 2);
> 
> ... while you properly use uint32_t here, ...
> 
> > +    union IO_APIC_reg_00 reg_00 = { .raw = reg_00_raw };
> > +    union IO_APIC_reg_01 reg_01 = { .raw = reg_01_raw };
> > +    union IO_APIC_reg_02 reg_02 = { .raw = reg_02_raw };
> >  
> >      if ( reg_00.raw == -1 && reg_01.raw == -1 && reg_02.raw == -1 )
> >      {
> > --- a/xen/arch/x86/mpparse.c
> > +++ b/xen/arch/x86/mpparse.c
> > @@ -798,11 +798,12 @@ void __init mp_register_lapic_address (
> >  
> >  int mp_register_lapic(u32 id, bool enabled, bool hotplug)
> >  {
> > +	u32 apic = apic_read(APIC_LVR);
> 
> ... why the being-phased-out u32 here?
> 
> Jan
> 
> >  	struct mpc_config_processor processor = {
> >  		.mpc_type = MP_PROCESSOR,
> >  		/* Note: We don't fill in fields not consumed anywhere. */
> >  		.mpc_apicid = id,
> > -		.mpc_apicver = GET_APIC_VERSION(apic_read(APIC_LVR)),
> > +		.mpc_apicver = GET_APIC_VERSION(apic),
> >  		.mpc_cpuflag = (enabled ? CPU_ENABLED : 0) |
> >  			       (id == boot_cpu_physical_apicid ?
> >  				CPU_BOOTPROCESSOR : 0),
> > --- a/xen/arch/x86/setup.c
> > +++ b/xen/arch/x86/setup.c
> > @@ -885,13 +885,14 @@ static struct domain *__init create_dom0(const module_t *image,
> >  {
> >      static char __initdata cmdline[MAX_GUEST_CMDLINE];
> >  
> > +    unsigned int max_vcpus = dom0_max_vcpus();
> >      struct xen_domctl_createdomain dom0_cfg = {
> >          .flags = IS_ENABLED(CONFIG_TBOOT) ? XEN_DOMCTL_CDF_s3_integrity : 0,
> >          .max_evtchn_port = -1,
> >          .max_grant_frames = -1,
> >          .max_maptrack_frames = -1,
> >          .grant_opts = XEN_DOMCTL_GRANT_version(opt_gnttab_max_version),
> > -        .max_vcpus = dom0_max_vcpus(),
> > +        .max_vcpus = max_vcpus,
> >          .arch = {
> >              .misc_flags = opt_dom0_msr_relaxed ? XEN_X86_MSR_RELAXED : 0,
> >          },
> 

Re: [XEN PATCH v4 3/4] xen/x86: address violations of MISRA C:2012 Rule 13.1

[Jan Beulich]

On 07.02.2024 01:56, Stefano Stabellini wrote:
> On Tue, 6 Feb 2024, Jan Beulich wrote:
>> On 02.02.2024 16:16, Simone Ballarin wrote:
>>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>>
>>> This patch moves expressions with side-effects into new variables before
>>> the initializer lists.
>>>
>>> No functional changes.
>>>
>>> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
>>
>> To be honest, I don't like this. It's more code for no gain. Really its
>> hampering clarity imo. I'm willing to be convinced otherwise, but for
>> now this gets a nack from me.
> 
> Which part of the patch you don't like? The changes to
> bad_ioapic_register?

Really all of them. bad_ioapic_register() is merely worst.

Jan

Re: [XEN PATCH v4 3/4] xen/x86: address violations of MISRA C:2012 Rule 13.1

[Simone Ballarin]

On 06/02/24 14:13, Jan Beulich wrote:
> On 02.02.2024 16:16, Simone Ballarin wrote:
>> Rule 13.1: Initializer lists shall not contain persistent side effects
>>
>> This patch moves expressions with side-effects into new variables before
>> the initializer lists.
>>
>> No functional changes.
>>
>> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
> 
> To be honest, I don't like this. It's more code for no gain. Really its
> hampering clarity imo. I'm willing to be convinced otherwise, but for
> now this gets a nack from me.
> 
> As an aside, ...
> 
>> --- a/xen/arch/x86/io_apic.c
>> +++ b/xen/arch/x86/io_apic.c
>> @@ -2559,9 +2559,12 @@ integer_param("max_gsi_irqs", max_gsi_irqs);
>>   
>>   static __init bool bad_ioapic_register(unsigned int idx)
>>   {
>> -    union IO_APIC_reg_00 reg_00 = { .raw = io_apic_read(idx, 0) };
>> -    union IO_APIC_reg_01 reg_01 = { .raw = io_apic_read(idx, 1) };
>> -    union IO_APIC_reg_02 reg_02 = { .raw = io_apic_read(idx, 2) };
>> +    uint32_t reg_00_raw = io_apic_read(idx, 0);
>> +    uint32_t reg_01_raw = io_apic_read(idx, 1);
>> +    uint32_t reg_02_raw = io_apic_read(idx, 2);

I'll propose a deviation for these single item initializers.

> 
> ... while you properly use uint32_t here, ...
> 
>> +    union IO_APIC_reg_00 reg_00 = { .raw = reg_00_raw };
>> +    union IO_APIC_reg_01 reg_01 = { .raw = reg_01_raw };
>> +    union IO_APIC_reg_02 reg_02 = { .raw = reg_02_raw };
>>   
>>       if ( reg_00.raw == -1 && reg_01.raw == -1 && reg_02.raw == -1 )
>>       {
>> --- a/xen/arch/x86/mpparse.c
>> +++ b/xen/arch/x86/mpparse.c
>> @@ -798,11 +798,12 @@ void __init mp_register_lapic_address (
>>   
>>   int mp_register_lapic(u32 id, bool enabled, bool hotplug)
>>   {
>> +	u32 apic = apic_read(APIC_LVR);> 
> ... why the being-phased-out u32 here?
> 

It was just to be coherent with the type of id.
I will use uint32_t in the next submission.

> Jan
> 
>>   	struct mpc_config_processor processor = {
>>   		.mpc_type = MP_PROCESSOR,
>>   		/* Note: We don't fill in fields not consumed anywhere. */
>>   		.mpc_apicid = id,
>> -		.mpc_apicver = GET_APIC_VERSION(apic_read(APIC_LVR)),
>> +		.mpc_apicver = GET_APIC_VERSION(apic),
>>   		.mpc_cpuflag = (enabled ? CPU_ENABLED : 0) |
>>   			       (id == boot_cpu_physical_apicid ?
>>   				CPU_BOOTPROCESSOR : 0),
>> --- a/xen/arch/x86/setup.c
>> +++ b/xen/arch/x86/setup.c
>> @@ -885,13 +885,14 @@ static struct domain *__init create_dom0(const module_t *image,
>>   {
>>       static char __initdata cmdline[MAX_GUEST_CMDLINE];
>>   
>> +    unsigned int max_vcpus = dom0_max_vcpus();
>>       struct xen_domctl_createdomain dom0_cfg = {
>>           .flags = IS_ENABLED(CONFIG_TBOOT) ? XEN_DOMCTL_CDF_s3_integrity : 0,
>>           .max_evtchn_port = -1,
>>           .max_grant_frames = -1,
>>           .max_maptrack_frames = -1,
>>           .grant_opts = XEN_DOMCTL_GRANT_version(opt_gnttab_max_version),
>> -        .max_vcpus = dom0_max_vcpus(),
>> +        .max_vcpus = max_vcpus,
>>           .arch = {
>>               .misc_flags = opt_dom0_msr_relaxed ? XEN_X86_MSR_RELAXED : 0,
>>           },
> 

-- 
Simone Ballarin, M.Sc.

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

[XEN PATCH v4 4/4] eclair: move function and macro properties outside ECLAIR

[Simone Ballarin]

From: Maria Celeste Cesario <maria.celeste.cesario@bugseng.com>

Function and macro properties contained in ECLAIR/call_properties.ecl are of
general interest: this patch moves these annotations in a generaric JSON file
in docs. In this way, they can be exploited for other purposes (i.e. documentation,
other tools).

Add rst file containing explanation on how to update function_macro_properties.json.
Add script to convert the JSON file in ECL configurations.
Remove ECLAIR/call_properties.ecl: the file is now automatically generated from
the JSON file.

Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>
Signed-off-by: Simone Ballarin  <simone.ballarin@bugseng.com>

---
Changes in v4:
- add missing script for converting the JSON file in ECL configurations;
- improve commit message;
- remove call_properties.ecs.
---
 .../eclair_analysis/ECLAIR/analysis.ecl       |   1 +
 .../ECLAIR/call_properties.ecl                | 128 ---
 automation/eclair_analysis/prepare.sh         |   2 +
 automation/eclair_analysis/propertyparser.py  |  37 +
 docs/function_macro_properties.json           | 841 ++++++++++++++++++
 docs/function_macro_properties.rst            |  58 ++
 6 files changed, 939 insertions(+), 128 deletions(-)
 delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl
 create mode 100644 automation/eclair_analysis/propertyparser.py
 create mode 100644 docs/function_macro_properties.json
 create mode 100644 docs/function_macro_properties.rst

diff --git a/automation/eclair_analysis/ECLAIR/analysis.ecl b/automation/eclair_analysis/ECLAIR/analysis.ecl
index a604582da3..684c5b0b39 100644
--- a/automation/eclair_analysis/ECLAIR/analysis.ecl
+++ b/automation/eclair_analysis/ECLAIR/analysis.ecl
@@ -30,6 +30,7 @@ if(not(scheduled_analysis),
 -eval_file=deviations.ecl
 -eval_file=call_properties.ecl
 -eval_file=tagging.ecl
+-eval_file=properties.ecl
 -eval_file=concat(set,".ecl")
 
 -doc="Hide reports in external code."
diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/eclair_analysis/ECLAIR/call_properties.ecl
deleted file mode 100644
index c2b2a6182e..0000000000
--- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
+++ /dev/null
@@ -1,128 +0,0 @@
-
--call_properties+={"name(printk)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"name(debugtrace_printk)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"name(panic)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"macro(^domain_crash$)", {"pointee_write(2..=never)", "taken()"}}
--call_properties+={"macro(^(g?d|mm_)?printk$)", {"pointee_write(2..=never)", "taken()"}}
--call_properties+={"macro(^guest_bug_on_failed$)", {"pointee_write(1=never)", "taken()"}}
--call_properties+={"macro(^spin_lock_init_prof$)", {"pointee_write(2=never)", "taken()"}}
--call_properties+={"macro(^sched_test_func$)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"macro(^dev_(info|warn)$)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"macro(^PAGING_DEBUG$)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"macro(^ACPI_(WARNING|ERROR|INFO)$)", {"pointee_write(1..=never)", "taken()"}}
--call_properties+={"name(fdt_get_property_by_offset_)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(read_atomic_size)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(device_tree_get_reg)", {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}}
--call_properties+={"name(dt_get_range)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}}
--call_properties+={"name(parse_static_mem_prop)", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}}
--call_properties+={"name(get_ttbr_and_gran_64bit)", {"pointee_write(1..2=always)", "pointee_read(1..2=never)", "taken()"}}
--call_properties+={"name(hvm_emulate_init_once)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(__vmread)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(hvm_pci_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(vpci_mmcfg_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(x86emul_decode)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(unmap_grant_ref)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(arm_smmu_cmdq_build_cmd)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(pci_size_mem_bar)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
--call_properties+={"name(_hvm_read_entry)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(hvm_map_guest_frame_rw)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(guest_cpuid)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
--call_properties+={"name(epte_get_entry_emt)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}}
--call_properties+={"name(mcheck_mca_logout)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(set_field_in_reg_u32)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}}
--call_properties+={"name(alloc_affinity_masks)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(xasprintf)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(find_non_smt)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(call_rcu)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(getdomaininfo)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"^MAPPING_(INSERT|SEARCH)\\(.*$", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}}
--call_properties+={"name(FormatDec)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(FormatHex)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(p2m_get_ioreq_server)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(elf_memset_unchecked)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(set_iommu_pte_present)", {"pointee_write(7=always)", "pointee_read(7=never)", "taken()"}}
--call_properties+={"name(clear_iommu_pte_present)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
--call_properties+={"name(vcpu_runstate_get)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(va_start)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(sgi_target_init)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(get_hw_residencies)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(x86_cpu_policy_to_featureset)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"^simple_strtou?ll?\\(.*$", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(msi_compose_msg)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(print_tainted)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(get_hvm_registers)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(x86_insn_modrm)", {"pointee_write(2..3=always)", "pointee_read(2..3=never)", "taken()"}}
--call_properties+={"name(cpuid_count_leaf)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--call_properties+={"name(rcu_lock_remote_domain_by_id)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(cpuid_count)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}}
--call_properties+={"name(efi_boot_mem_unused)", {"pointee_write(1..=always)", "pointee_read(1..=never)", "taken()"}}
--call_properties+={"name(collect_time_info)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
--call_properties+={"name(setup_xstate_comp)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--call_properties+={"name(map_domain_gfn)", {"pointee_read(5=never)", "taken()"}}
--call_properties+={"name(fdt_getprop)", {"pointee_read(4=never)", "taken()"}}
--call_properties+={"name(fdt_get_name)", {"pointee_read(3=never)", "taken()"}}
--call_properties+={"name(fdt_get_property)", {"pointee_read(4=never)", "taken()"}}
--call_properties+={"name(pci_get_host_bridge_segment)", {"pointee_read(2=never)", "taken()"}}
--call_properties+={"name(dt_get_property)", {"pointee_read(3=never)", "taken()"}}
--call_properties+={"name(dt_property_read_u32)", {"pointee_read(3=never)", "taken()"}}
--call_properties+={"name(dt_device_get_paddr)", {"pointee_read(3..4=never)", "taken()"}}
--call_properties+={"name(get_evtchn_dt_property)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}}
--call_properties+={"name(setup_chosen_node)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}}
--call_properties+={"name(queue_remove_raw)", {"pointee_read(2=never)", "taken()"}}
--call_properties+={"macro(^memset$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--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()"}}
--doc_end
-
--doc_begin="Property inferred as a consequence of the semantics of dt_set_cell"
--call_properties+={"name(set_interrupt)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--doc_end
-
--doc_begin="Property inferred as a consequence of the semantics of __p2m_get_mem_access"
--call_properties+={"name(p2m_get_mem_access)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
--doc_end
-
--doc_begin="This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}"
--call_properties+={"name(alloc_cpumask_var)", {"pointee_write(1=maybe)", "pointee_read(1=never)", "taken()"}}
--doc_end
-
--doc_begin="Property inferred as a consequence of the semantics of alloc_cpumask_var"
--call_properties+={"name(xenctl_bitmap_to_cpumask)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--doc_end
-
--doc_begin="The call to bitmap_and causes the pointee of dstp to be always written"
--call_properties+={"^cpumask_(and|andnot|clear|copy|complement).*$", {"pointee_write(1=always)", "pointee_read(1=never)" "taken()"}}
--call_properties+={"^bitmap_(andnot|complement|fill).*$", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
--doc_end
-
--doc_begin="The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source.
-Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller."
--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
diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
index fe9d16e48e..47b2a2f32a 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -43,4 +43,6 @@ fi
     make -f "${script_dir}/Makefile.prepare" prepare
     # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
     scripts/xen-analysis.py --run-eclair --no-build --no-clean
+    # Translate function-properties.json into ECLAIR properties
+    python3 ${script_dir}/propertyparser.py
 )
diff --git a/automation/eclair_analysis/propertyparser.py b/automation/eclair_analysis/propertyparser.py
new file mode 100644
index 0000000000..0d02f505a6
--- /dev/null
+++ b/automation/eclair_analysis/propertyparser.py
@@ -0,0 +1,37 @@
+import json
+import os
+
+script_dir = os.path.dirname(__file__)
+properties_path = os.path.join(script_dir, "../../docs/function_macro_properties.json")
+output_path   = os.path.join(script_dir, "ECLAIR/call_properties.ecl")
+
+with open(properties_path) as fp:
+    properties = json.load(fp)['content']
+
+ecl = open(output_path, 'w')
+
+for record in properties:
+
+    string = "-call_properties+={\""
+    if record['type'] == "function":
+        string += f"{record['value']}\", {{".replace("\\", "\\\\")
+    else:
+        string += f"{record['type']}({record['value']})\", {{".replace("\\", "\\\\")
+
+    i=0
+    for prop in record['properties'].items():
+        if prop[0] == 'attribute':
+            string += prop[1]
+            i+=1
+        else:
+            string += f"\"{prop[0]}({prop[1]})\""
+            i+=1
+
+        if i<len(record['properties']):
+            string += ", "
+        else:
+            string +="}}\n"
+
+    ecl.write(string)
+
+ecl.close()
diff --git a/docs/function_macro_properties.json b/docs/function_macro_properties.json
new file mode 100644
index 0000000000..74058297b5
--- /dev/null
+++ b/docs/function_macro_properties.json
@@ -0,0 +1,841 @@
+{
+   "version": "1.0",
+   "content": [
+      {
+         "type": "function",
+         "value": "^printk.*$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^debugtrace_printk.*$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^panic.*$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^domain_crash$",
+         "properties":{
+            "pointee_write": "2..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^(g?d|mm_)?printk$",
+         "properties":{
+            "pointee_write": "2..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^guest_bug_on_failed$",
+         "properties":{
+            "pointee_write": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^spin_lock_init_prof$",
+         "properties":{
+            "pointee_write": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^sched_test_func$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^dev_(info|warn)$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^PAGING_DEBUG$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^ACPI_(WARNING|ERROR|INFO)$",
+         "properties":{
+            "pointee_write": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^fdt_get_property_by_offset_.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^read_atomic_size.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^device_tree_get_reg.*$",
+         "properties":{
+            "pointee_write": "4..=always",
+            "pointee_read": "4..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^dt_get_range.*$",
+         "properties":{
+            "pointee_write": "3..=always",
+            "pointee_read": "3..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^parse_static_mem_prop.*$",
+         "properties":{
+            "pointee_write": "2..=always",
+            "pointee_read": "2..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_ttbr_and_gran_64bit.*$",
+         "properties":{
+            "pointee_write": "1..2=always",
+            "pointee_read": "1..2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^hvm_emulate_init_once.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^__vmread.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^hvm_pci_decode_addr.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^vpci_mmcfg_decode_addr.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^x86emul_decode.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^unmap_grant_ref.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^arm_smmu_cmdq_build_cmd.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^pci_size_mem_bar.*$",
+         "properties":{
+            "pointee_write": "4=always",
+            "pointee_read": "4=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^_hvm_read_entry.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^hvm_map_guest_frame_rw.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^guest_cpuid.*$",
+         "properties":{
+            "pointee_write": "4=always",
+            "pointee_read": "4=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^epte_get_entry_emt.*$",
+         "properties":{
+            "pointee_write": "5=always",
+            "pointee_read": "5=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^mcheck_mca_logout.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^set_field_in_reg_u32.*$",
+         "properties":{
+            "pointee_write": "5=always",
+            "pointee_read": "5=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^alloc_affinity_masks.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^xasprintf.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^find_non_smt.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^call_rcu.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^getdomaininfo.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^MAPPING_(INSERT|SEARCH)\\(.*$",
+         "properties":{
+            "pointee_write": "2..=always",
+            "pointee_read": "2..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^FormatDec.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^FormatHex.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^p2m_get_ioreq_server.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^elf_memset_unchecked.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^set_iommu_pte_present.*$",
+         "properties":{
+            "pointee_write": "7=always",
+            "pointee_read": "7=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^clear_iommu_pte_present.*$",
+         "properties":{
+            "pointee_write": "4=always",
+            "pointee_read": "4=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^vcpu_runstate_get.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^va_start.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^sgi_target_init.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_hw_residencies.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^x86_cpu_policy_to_featureset.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^simple_strtou?ll?\\(.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^msi_compose_msg.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^print_tainted.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_hvm_registers.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^x86_insn_modrm.*$",
+         "properties":{
+            "pointee_write": "2..3=always",
+            "pointee_read": "2..3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^cpuid_count_leaf.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^rcu_lock_remote_domain_by_id.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^cpuid_count.*$",
+         "properties":{
+            "pointee_write": "3..=always",
+            "pointee_read": "3..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^.*efi_boot_mem_unused.*$",
+         "properties":{
+            "pointee_write": "1..=always",
+            "pointee_read": "1..=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^collect_time_info.*$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^setup_xstate_comp.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^map_domain_gfn.*$",
+         "properties":{
+            "pointee_read": "5=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^fdt_getprop.*$",
+         "properties":{
+            "pointee_read": "4=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^fdt_get_name.*$",
+         "properties":{
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^fdt_get_property.*$",
+         "properties":{
+            "pointee_read": "4=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^pci_get_host_bridge_segment.*$",
+         "properties":{
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^dt_get_property.*$",
+         "properties":{
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^dt_property_read_u32.*$",
+         "properties":{
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^dt_device_get_paddr.*$",
+         "properties":{
+            "pointee_read": "3..4=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_evtchn_dt_property.*$",
+         "properties":{
+            "pointee_write": "2..3=maybe",
+            "pointee_read": "2..3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^setup_chosen_node.*$",
+         "properties":{
+            "pointee_write": "2..3=maybe",
+            "pointee_read": "2..3=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^queue_remove_raw.*$",
+         "properties":{
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^memset$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^va_start$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^memcmp$",
+         "properties":{
+            "pointee_write": "1..2=never",
+            "taken": ""
+         }
+      },
+      {
+         "type": "macro",
+         "value": "^memcpy$",
+         "properties":{
+            "pointee_write": "1=always&&2..=never",
+            "pointee_read": "1=never&&2..=always",
+            "taken": ""
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_cpu_info.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^pdx_to_pfn.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^is_pci_passthrough_enabled.*$",
+         "properties":{
+            "attribute": "const"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_cycles.*$",
+         "properties":{
+            "attribute": "noeffect"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^msi_gflags.*$",
+         "properties":{
+            "attribute": "const"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^hvm_save_size.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^cpu_has.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^boot_cpu_has.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^get_cpu_info.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^put_pte_flags.*$",
+         "properties":{
+            "attribute": "const"
+         }
+      },
+      {
+         "type": "function",
+         "value": "^is_pv_cpu.*$",
+         "properties":{
+            "attribute": "pure"
+         }
+      },
+      {
+         "description": "Property inferred as a consequence of the semantics of device_tree_get_reg",
+         "type": "function",
+         "value": "^acquire_static_memory_bank.*$",
+         "properties":{
+            "pointee_write": "4..=always",
+            "pointee_read": "4..=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "Property inferred as a consequence of the semantics of dt_set_cell",
+         "type": "function",
+         "value": "^set_interrupt.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "description":"Property inferred as a consequence of the semantics of __p2m_get_mem_access",
+         "type": "function",
+         "value": "^p2m_get_mem_access.*$",
+         "properties":{
+            "pointee_write": "3=always",
+            "pointee_read": "3=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}",
+         "type": "function",
+         "value": "^alloc_cpumask_var.*$",
+         "properties":{
+            "pointee_write": "1=maybe",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "Property inferred as a consequence of the semantics of alloc_cpumask_var",
+         "type": "function",
+         "value": "^xenctl_bitmap_to_cpumask.*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "The call to bitmap_and causes the pointee of dstp to be always written",
+         "type": "function",
+         "value": "^cpumask_(and|andnot|clear|copy|complement).*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "The call to bitmap_and causes the pointee of dstp to be always written",
+         "type": "function",
+         "value": "^bitmap_(andnot|complement|fill).*$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source. Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller.",
+         "type": "macro",
+         "value": "^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$",
+         "properties":{
+            "pointee_write": "1=always",
+            "pointee_read": "1=never",
+            "taken": ""
+         }
+      },
+      {
+         "description":"The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source. Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller.",
+         "type": "macro",
+         "value": "^(__)?copy_to_(guest|compat)(_offset)?$",
+         "properties":{
+            "pointee_write": "2=always",
+            "pointee_read": "2=never",
+            "taken": ""
+         }
+      },
+      {
+         "description": "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.",
+         "type": "function",
+         "value": "^read_u(8|16|32|64|int)_atomic.*$",
+         "properties":{
+            "attribute": "noeffect"
+         }
+      },
+      {
+         "description": "Functions generated by TYPE_SAFE are const.",
+         "type": "function",
+         "value": "^(mfn|gfn|pfn)_x\\(.*$",
+         "properties":{
+            "attribute": "const"
+         }
+      },
+      {
+         "description": "Functions generated by TYPE_SAFE are const.",
+         "type": "function",
+         "value": "^_(mfn|gfn|pfn)\\(.*$",
+         "properties":{
+            "attribute": "const"
+         }
+      }
+   ]
+}
diff --git a/docs/function_macro_properties.rst b/docs/function_macro_properties.rst
new file mode 100644
index 0000000000..ea6fb5cf1f
--- /dev/null
+++ b/docs/function_macro_properties.rst
@@ -0,0 +1,58 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+Properties list for Xen
+=======================
+
+Some functions and macros are found to have properties relevant to
+the Xen codebase. For this reason, the file docs/properties.json
+contains all the needed properties.
+
+Here is an example of the properties.json file::
+
+  {
+     "version": "1.0",
+     "content": [
+        {
+           "description": ""
+           "type": "function",       // required
+           "value:": "^printk*.$",   // required
+           "properties":{
+              "pointee_write": "1..2=never",
+              "pointee_read": "",
+              "taken": ""
+              "attribute": ""
+           }
+        }
+     ]
+  }
+
+Here is an explanation of the fields inside an object of the "content" array:
+
+ - description: a brief description of why the properties apply
+ - type: this is the kind of the element called: it may be either ``macro`` or ``function``
+ - value: must be a regex, starting with ^ and ending with $ and matching function fully
+   qualified name or macro name.
+ - properties: a list of properties applied to said function.
+   Possible values are:
+
+    - pointee_write: indicate the write use for call arguments that correspond to
+      parameters whose pointee types are non-const
+    - pointee_read: indicate the read use for call arguments that correspond to
+      parameters whose pointee types are non-const
+    - taken: indicates that the specified address arguments may be stored in objects
+      that persist after the function has ceased to exist (excluding the returned value);
+      address arguments not listed are never taken
+    - attribute: attributes a function may have. Possible values are pure, const and noeffect.
+
+   pointee_read and pointee_write use a specific kind of argument, structured as pointee_arg=rw:
+
+    - pointee_arg: argument index for callee. Index 0 refers to the return value,
+      the indices of the arguments start from 1. It can be either a single value or a range.
+    - rw: a value that's either always, maybe or never
+
+       - always: for pointee_read: argument pointee is expected to be fully read in the function body,
+         for pointee_write: argument pointee is fully initialized at function exit
+       - maybe: for pointee_read: argument pointee may be expected to be read in the function body,
+         for pointee_write: argument pointee may be written by function body
+       - never: for pointee_read: argument pointee is not expected to be read in the function body,
+         for pointee_write: argument pointee is never written by function body
-- 
2.34.1

Re: [XEN PATCH v4 4/4] eclair: move function and macro properties outside ECLAIR

[Stefano Stabellini]

On Fri, 2 Feb 2024, Simone Ballarin wrote:
> From: Maria Celeste Cesario <maria.celeste.cesario@bugseng.com>
> 
> Function and macro properties contained in ECLAIR/call_properties.ecl are of
> general interest: this patch moves these annotations in a generaric JSON file
> in docs. In this way, they can be exploited for other purposes (i.e. documentation,
> other tools).
> 
> Add rst file containing explanation on how to update function_macro_properties.json.
> Add script to convert the JSON file in ECL configurations.
> Remove ECLAIR/call_properties.ecl: the file is now automatically generated from
> the JSON file.
> 
> Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>
> Signed-off-by: Simone Ballarin  <simone.ballarin@bugseng.com>

This is much better, thank you!

Acked-by: Stefano Stabellini <sstabellini@kernel.org>

> ---
> Changes in v4:
> - add missing script for converting the JSON file in ECL configurations;
> - improve commit message;
> - remove call_properties.ecs.
> ---
>  .../eclair_analysis/ECLAIR/analysis.ecl       |   1 +
>  .../ECLAIR/call_properties.ecl                | 128 ---
>  automation/eclair_analysis/prepare.sh         |   2 +
>  automation/eclair_analysis/propertyparser.py  |  37 +
>  docs/function_macro_properties.json           | 841 ++++++++++++++++++
>  docs/function_macro_properties.rst            |  58 ++
>  6 files changed, 939 insertions(+), 128 deletions(-)
>  delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl
>  create mode 100644 automation/eclair_analysis/propertyparser.py
>  create mode 100644 docs/function_macro_properties.json
>  create mode 100644 docs/function_macro_properties.rst
> 
> diff --git a/automation/eclair_analysis/ECLAIR/analysis.ecl b/automation/eclair_analysis/ECLAIR/analysis.ecl
> index a604582da3..684c5b0b39 100644
> --- a/automation/eclair_analysis/ECLAIR/analysis.ecl
> +++ b/automation/eclair_analysis/ECLAIR/analysis.ecl
> @@ -30,6 +30,7 @@ if(not(scheduled_analysis),
>  -eval_file=deviations.ecl
>  -eval_file=call_properties.ecl
>  -eval_file=tagging.ecl
> +-eval_file=properties.ecl
>  -eval_file=concat(set,".ecl")
>  
>  -doc="Hide reports in external code."
> diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> deleted file mode 100644
> index c2b2a6182e..0000000000
> --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
> +++ /dev/null
> @@ -1,128 +0,0 @@
> -
> --call_properties+={"name(printk)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"name(debugtrace_printk)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"name(panic)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"macro(^domain_crash$)", {"pointee_write(2..=never)", "taken()"}}
> --call_properties+={"macro(^(g?d|mm_)?printk$)", {"pointee_write(2..=never)", "taken()"}}
> --call_properties+={"macro(^guest_bug_on_failed$)", {"pointee_write(1=never)", "taken()"}}
> --call_properties+={"macro(^spin_lock_init_prof$)", {"pointee_write(2=never)", "taken()"}}
> --call_properties+={"macro(^sched_test_func$)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"macro(^dev_(info|warn)$)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"macro(^PAGING_DEBUG$)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"macro(^ACPI_(WARNING|ERROR|INFO)$)", {"pointee_write(1..=never)", "taken()"}}
> --call_properties+={"name(fdt_get_property_by_offset_)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(read_atomic_size)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(device_tree_get_reg)", {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}}
> --call_properties+={"name(dt_get_range)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}}
> --call_properties+={"name(parse_static_mem_prop)", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}}
> --call_properties+={"name(get_ttbr_and_gran_64bit)", {"pointee_write(1..2=always)", "pointee_read(1..2=never)", "taken()"}}
> --call_properties+={"name(hvm_emulate_init_once)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(__vmread)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(hvm_pci_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(vpci_mmcfg_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(x86emul_decode)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(unmap_grant_ref)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(arm_smmu_cmdq_build_cmd)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(pci_size_mem_bar)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
> --call_properties+={"name(_hvm_read_entry)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(hvm_map_guest_frame_rw)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(guest_cpuid)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
> --call_properties+={"name(epte_get_entry_emt)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}}
> --call_properties+={"name(mcheck_mca_logout)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(set_field_in_reg_u32)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}}
> --call_properties+={"name(alloc_affinity_masks)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(xasprintf)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(find_non_smt)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(call_rcu)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(getdomaininfo)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"^MAPPING_(INSERT|SEARCH)\\(.*$", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}}
> --call_properties+={"name(FormatDec)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(FormatHex)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(p2m_get_ioreq_server)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(elf_memset_unchecked)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(set_iommu_pte_present)", {"pointee_write(7=always)", "pointee_read(7=never)", "taken()"}}
> --call_properties+={"name(clear_iommu_pte_present)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}}
> --call_properties+={"name(vcpu_runstate_get)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(va_start)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(sgi_target_init)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(get_hw_residencies)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(x86_cpu_policy_to_featureset)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"^simple_strtou?ll?\\(.*$", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(msi_compose_msg)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(print_tainted)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(get_hvm_registers)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(x86_insn_modrm)", {"pointee_write(2..3=always)", "pointee_read(2..3=never)", "taken()"}}
> --call_properties+={"name(cpuid_count_leaf)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(rcu_lock_remote_domain_by_id)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(cpuid_count)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}}
> --call_properties+={"name(efi_boot_mem_unused)", {"pointee_write(1..=always)", "pointee_read(1..=never)", "taken()"}}
> --call_properties+={"name(collect_time_info)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(setup_xstate_comp)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --call_properties+={"name(map_domain_gfn)", {"pointee_read(5=never)", "taken()"}}
> --call_properties+={"name(fdt_getprop)", {"pointee_read(4=never)", "taken()"}}
> --call_properties+={"name(fdt_get_name)", {"pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(fdt_get_property)", {"pointee_read(4=never)", "taken()"}}
> --call_properties+={"name(pci_get_host_bridge_segment)", {"pointee_read(2=never)", "taken()"}}
> --call_properties+={"name(dt_get_property)", {"pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(dt_property_read_u32)", {"pointee_read(3=never)", "taken()"}}
> --call_properties+={"name(dt_device_get_paddr)", {"pointee_read(3..4=never)", "taken()"}}
> --call_properties+={"name(get_evtchn_dt_property)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}}
> --call_properties+={"name(setup_chosen_node)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}}
> --call_properties+={"name(queue_remove_raw)", {"pointee_read(2=never)", "taken()"}}
> --call_properties+={"macro(^memset$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --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()"}}
> --doc_end
> -
> --doc_begin="Property inferred as a consequence of the semantics of dt_set_cell"
> --call_properties+={"name(set_interrupt)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --doc_end
> -
> --doc_begin="Property inferred as a consequence of the semantics of __p2m_get_mem_access"
> --call_properties+={"name(p2m_get_mem_access)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}}
> --doc_end
> -
> --doc_begin="This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}"
> --call_properties+={"name(alloc_cpumask_var)", {"pointee_write(1=maybe)", "pointee_read(1=never)", "taken()"}}
> --doc_end
> -
> --doc_begin="Property inferred as a consequence of the semantics of alloc_cpumask_var"
> --call_properties+={"name(xenctl_bitmap_to_cpumask)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --doc_end
> -
> --doc_begin="The call to bitmap_and causes the pointee of dstp to be always written"
> --call_properties+={"^cpumask_(and|andnot|clear|copy|complement).*$", {"pointee_write(1=always)", "pointee_read(1=never)" "taken()"}}
> --call_properties+={"^bitmap_(andnot|complement|fill).*$", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
> --doc_end
> -
> --doc_begin="The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source.
> -Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller."
> --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
> diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
> index fe9d16e48e..47b2a2f32a 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -43,4 +43,6 @@ fi
>      make -f "${script_dir}/Makefile.prepare" prepare
>      # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
>      scripts/xen-analysis.py --run-eclair --no-build --no-clean
> +    # Translate function-properties.json into ECLAIR properties
> +    python3 ${script_dir}/propertyparser.py
>  )
> diff --git a/automation/eclair_analysis/propertyparser.py b/automation/eclair_analysis/propertyparser.py
> new file mode 100644
> index 0000000000..0d02f505a6
> --- /dev/null
> +++ b/automation/eclair_analysis/propertyparser.py
> @@ -0,0 +1,37 @@
> +import json
> +import os
> +
> +script_dir = os.path.dirname(__file__)
> +properties_path = os.path.join(script_dir, "../../docs/function_macro_properties.json")
> +output_path   = os.path.join(script_dir, "ECLAIR/call_properties.ecl")
> +
> +with open(properties_path) as fp:
> +    properties = json.load(fp)['content']
> +
> +ecl = open(output_path, 'w')
> +
> +for record in properties:
> +
> +    string = "-call_properties+={\""
> +    if record['type'] == "function":
> +        string += f"{record['value']}\", {{".replace("\\", "\\\\")
> +    else:
> +        string += f"{record['type']}({record['value']})\", {{".replace("\\", "\\\\")
> +
> +    i=0
> +    for prop in record['properties'].items():
> +        if prop[0] == 'attribute':
> +            string += prop[1]
> +            i+=1
> +        else:
> +            string += f"\"{prop[0]}({prop[1]})\""
> +            i+=1
> +
> +        if i<len(record['properties']):
> +            string += ", "
> +        else:
> +            string +="}}\n"
> +
> +    ecl.write(string)
> +
> +ecl.close()
> diff --git a/docs/function_macro_properties.json b/docs/function_macro_properties.json
> new file mode 100644
> index 0000000000..74058297b5
> --- /dev/null
> +++ b/docs/function_macro_properties.json
> @@ -0,0 +1,841 @@
> +{
> +   "version": "1.0",
> +   "content": [
> +      {
> +         "type": "function",
> +         "value": "^printk.*$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^debugtrace_printk.*$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^panic.*$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^domain_crash$",
> +         "properties":{
> +            "pointee_write": "2..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^(g?d|mm_)?printk$",
> +         "properties":{
> +            "pointee_write": "2..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^guest_bug_on_failed$",
> +         "properties":{
> +            "pointee_write": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^spin_lock_init_prof$",
> +         "properties":{
> +            "pointee_write": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^sched_test_func$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^dev_(info|warn)$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^PAGING_DEBUG$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^ACPI_(WARNING|ERROR|INFO)$",
> +         "properties":{
> +            "pointee_write": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^fdt_get_property_by_offset_.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^read_atomic_size.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^device_tree_get_reg.*$",
> +         "properties":{
> +            "pointee_write": "4..=always",
> +            "pointee_read": "4..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^dt_get_range.*$",
> +         "properties":{
> +            "pointee_write": "3..=always",
> +            "pointee_read": "3..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^parse_static_mem_prop.*$",
> +         "properties":{
> +            "pointee_write": "2..=always",
> +            "pointee_read": "2..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_ttbr_and_gran_64bit.*$",
> +         "properties":{
> +            "pointee_write": "1..2=always",
> +            "pointee_read": "1..2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^hvm_emulate_init_once.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^__vmread.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^hvm_pci_decode_addr.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^vpci_mmcfg_decode_addr.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^x86emul_decode.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^unmap_grant_ref.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^arm_smmu_cmdq_build_cmd.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^pci_size_mem_bar.*$",
> +         "properties":{
> +            "pointee_write": "4=always",
> +            "pointee_read": "4=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^_hvm_read_entry.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^hvm_map_guest_frame_rw.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^guest_cpuid.*$",
> +         "properties":{
> +            "pointee_write": "4=always",
> +            "pointee_read": "4=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^epte_get_entry_emt.*$",
> +         "properties":{
> +            "pointee_write": "5=always",
> +            "pointee_read": "5=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^mcheck_mca_logout.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^set_field_in_reg_u32.*$",
> +         "properties":{
> +            "pointee_write": "5=always",
> +            "pointee_read": "5=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^alloc_affinity_masks.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^xasprintf.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^find_non_smt.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^call_rcu.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^getdomaininfo.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^MAPPING_(INSERT|SEARCH)\\(.*$",
> +         "properties":{
> +            "pointee_write": "2..=always",
> +            "pointee_read": "2..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^FormatDec.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^FormatHex.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^p2m_get_ioreq_server.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^elf_memset_unchecked.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^set_iommu_pte_present.*$",
> +         "properties":{
> +            "pointee_write": "7=always",
> +            "pointee_read": "7=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^clear_iommu_pte_present.*$",
> +         "properties":{
> +            "pointee_write": "4=always",
> +            "pointee_read": "4=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^vcpu_runstate_get.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^va_start.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^sgi_target_init.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_hw_residencies.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^x86_cpu_policy_to_featureset.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^simple_strtou?ll?\\(.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^msi_compose_msg.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^print_tainted.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_hvm_registers.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^x86_insn_modrm.*$",
> +         "properties":{
> +            "pointee_write": "2..3=always",
> +            "pointee_read": "2..3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^cpuid_count_leaf.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^rcu_lock_remote_domain_by_id.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^cpuid_count.*$",
> +         "properties":{
> +            "pointee_write": "3..=always",
> +            "pointee_read": "3..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^.*efi_boot_mem_unused.*$",
> +         "properties":{
> +            "pointee_write": "1..=always",
> +            "pointee_read": "1..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^collect_time_info.*$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^setup_xstate_comp.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^map_domain_gfn.*$",
> +         "properties":{
> +            "pointee_read": "5=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^fdt_getprop.*$",
> +         "properties":{
> +            "pointee_read": "4=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^fdt_get_name.*$",
> +         "properties":{
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^fdt_get_property.*$",
> +         "properties":{
> +            "pointee_read": "4=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^pci_get_host_bridge_segment.*$",
> +         "properties":{
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^dt_get_property.*$",
> +         "properties":{
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^dt_property_read_u32.*$",
> +         "properties":{
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^dt_device_get_paddr.*$",
> +         "properties":{
> +            "pointee_read": "3..4=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_evtchn_dt_property.*$",
> +         "properties":{
> +            "pointee_write": "2..3=maybe",
> +            "pointee_read": "2..3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^setup_chosen_node.*$",
> +         "properties":{
> +            "pointee_write": "2..3=maybe",
> +            "pointee_read": "2..3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^queue_remove_raw.*$",
> +         "properties":{
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^memset$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^va_start$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^memcmp$",
> +         "properties":{
> +            "pointee_write": "1..2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "macro",
> +         "value": "^memcpy$",
> +         "properties":{
> +            "pointee_write": "1=always&&2..=never",
> +            "pointee_read": "1=never&&2..=always",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_cpu_info.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^pdx_to_pfn.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^is_pci_passthrough_enabled.*$",
> +         "properties":{
> +            "attribute": "const"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_cycles.*$",
> +         "properties":{
> +            "attribute": "noeffect"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^msi_gflags.*$",
> +         "properties":{
> +            "attribute": "const"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^hvm_save_size.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^cpu_has.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^boot_cpu_has.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^get_cpu_info.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^put_pte_flags.*$",
> +         "properties":{
> +            "attribute": "const"
> +         }
> +      },
> +      {
> +         "type": "function",
> +         "value": "^is_pv_cpu.*$",
> +         "properties":{
> +            "attribute": "pure"
> +         }
> +      },
> +      {
> +         "description": "Property inferred as a consequence of the semantics of device_tree_get_reg",
> +         "type": "function",
> +         "value": "^acquire_static_memory_bank.*$",
> +         "properties":{
> +            "pointee_write": "4..=always",
> +            "pointee_read": "4..=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "Property inferred as a consequence of the semantics of dt_set_cell",
> +         "type": "function",
> +         "value": "^set_interrupt.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description":"Property inferred as a consequence of the semantics of __p2m_get_mem_access",
> +         "type": "function",
> +         "value": "^p2m_get_mem_access.*$",
> +         "properties":{
> +            "pointee_write": "3=always",
> +            "pointee_read": "3=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}",
> +         "type": "function",
> +         "value": "^alloc_cpumask_var.*$",
> +         "properties":{
> +            "pointee_write": "1=maybe",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "Property inferred as a consequence of the semantics of alloc_cpumask_var",
> +         "type": "function",
> +         "value": "^xenctl_bitmap_to_cpumask.*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "The call to bitmap_and causes the pointee of dstp to be always written",
> +         "type": "function",
> +         "value": "^cpumask_(and|andnot|clear|copy|complement).*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "The call to bitmap_and causes the pointee of dstp to be always written",
> +         "type": "function",
> +         "value": "^bitmap_(andnot|complement|fill).*$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source. Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller.",
> +         "type": "macro",
> +         "value": "^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$",
> +         "properties":{
> +            "pointee_write": "1=always",
> +            "pointee_read": "1=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description":"The .*copy_(to|from).* helpers all have a memcpy-like expectation that the destination is a copy of the source. Furthermore, their uses do initialize the involved variables as needed by futher uses in the caller.",
> +         "type": "macro",
> +         "value": "^(__)?copy_to_(guest|compat)(_offset)?$",
> +         "properties":{
> +            "pointee_write": "2=always",
> +            "pointee_read": "2=never",
> +            "taken": ""
> +         }
> +      },
> +      {
> +         "description": "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.",
> +         "type": "function",
> +         "value": "^read_u(8|16|32|64|int)_atomic.*$",
> +         "properties":{
> +            "attribute": "noeffect"
> +         }
> +      },
> +      {
> +         "description": "Functions generated by TYPE_SAFE are const.",
> +         "type": "function",
> +         "value": "^(mfn|gfn|pfn)_x\\(.*$",
> +         "properties":{
> +            "attribute": "const"
> +         }
> +      },
> +      {
> +         "description": "Functions generated by TYPE_SAFE are const.",
> +         "type": "function",
> +         "value": "^_(mfn|gfn|pfn)\\(.*$",
> +         "properties":{
> +            "attribute": "const"
> +         }
> +      }
> +   ]
> +}
> diff --git a/docs/function_macro_properties.rst b/docs/function_macro_properties.rst
> new file mode 100644
> index 0000000000..ea6fb5cf1f
> --- /dev/null
> +++ b/docs/function_macro_properties.rst
> @@ -0,0 +1,58 @@
> +.. SPDX-License-Identifier: CC-BY-4.0
> +
> +Properties list for Xen
> +=======================
> +
> +Some functions and macros are found to have properties relevant to
> +the Xen codebase. For this reason, the file docs/properties.json
> +contains all the needed properties.
> +
> +Here is an example of the properties.json file::
> +
> +  {
> +     "version": "1.0",
> +     "content": [
> +        {
> +           "description": ""
> +           "type": "function",       // required
> +           "value:": "^printk*.$",   // required
> +           "properties":{
> +              "pointee_write": "1..2=never",
> +              "pointee_read": "",
> +              "taken": ""
> +              "attribute": ""
> +           }
> +        }
> +     ]
> +  }
> +
> +Here is an explanation of the fields inside an object of the "content" array:
> +
> + - description: a brief description of why the properties apply
> + - type: this is the kind of the element called: it may be either ``macro`` or ``function``
> + - value: must be a regex, starting with ^ and ending with $ and matching function fully
> +   qualified name or macro name.
> + - properties: a list of properties applied to said function.
> +   Possible values are:
> +
> +    - pointee_write: indicate the write use for call arguments that correspond to
> +      parameters whose pointee types are non-const
> +    - pointee_read: indicate the read use for call arguments that correspond to
> +      parameters whose pointee types are non-const
> +    - taken: indicates that the specified address arguments may be stored in objects
> +      that persist after the function has ceased to exist (excluding the returned value);
> +      address arguments not listed are never taken
> +    - attribute: attributes a function may have. Possible values are pure, const and noeffect.
> +
> +   pointee_read and pointee_write use a specific kind of argument, structured as pointee_arg=rw:
> +
> +    - pointee_arg: argument index for callee. Index 0 refers to the return value,
> +      the indices of the arguments start from 1. It can be either a single value or a range.
> +    - rw: a value that's either always, maybe or never
> +
> +       - always: for pointee_read: argument pointee is expected to be fully read in the function body,
> +         for pointee_write: argument pointee is fully initialized at function exit
> +       - maybe: for pointee_read: argument pointee may be expected to be read in the function body,
> +         for pointee_write: argument pointee may be written by function body
> +       - never: for pointee_read: argument pointee is not expected to be read in the function body,
> +         for pointee_write: argument pointee is never written by function body
> -- 
> 2.34.1
> 

[REGRESSION] Re: [XEN PATCH v4 4/4] eclair: move function and macro properties outside ECLAIR

[Andrew Cooper]

On 02/02/2024 3:16 pm, Simone Ballarin wrote:
> From: Maria Celeste Cesario <maria.celeste.cesario@bugseng.com>
>
> Function and macro properties contained in ECLAIR/call_properties.ecl are of
> general interest: this patch moves these annotations in a generaric JSON file
> in docs. In this way, they can be exploited for other purposes (i.e. documentation,
> other tools).
>
> Add rst file containing explanation on how to update function_macro_properties.json.
> Add script to convert the JSON file in ECL configurations.
> Remove ECLAIR/call_properties.ecl: the file is now automatically generated from
> the JSON file.
>
> Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>
> Signed-off-by: Simone Ballarin  <simone.ballarin@bugseng.com>
>
> ---
> Changes in v4:
> - add missing script for converting the JSON file in ECL configurations;
> - improve commit message;
> - remove call_properties.ecs.
> ---
>  .../eclair_analysis/ECLAIR/analysis.ecl       |   1 +
>  .../ECLAIR/call_properties.ecl                | 128 ---
>  automation/eclair_analysis/prepare.sh         |   2 +
>  automation/eclair_analysis/propertyparser.py  |  37 +
>  docs/function_macro_properties.json           | 841 ++++++++++++++++++
>  docs/function_macro_properties.rst            |  58 ++
>  6 files changed, 939 insertions(+), 128 deletions(-)
>  delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl
>  create mode 100644 automation/eclair_analysis/propertyparser.py
>  create mode 100644 docs/function_macro_properties.json
>  create mode 100644 docs/function_macro_properties.rst

This breaks the Sphinx build.

checking consistency...
/local/xen.git/docs/function_macro_properties.rst: WARNING: document
isn't included in any toctree

Also, the top level of docs really isn't an appropriate place to put
it.  Everything else is in docs/misra/.

When you've moved the files, you'll need to edit docs/misra/index.rst to
fix the build.

~Andrew

Re: [REGRESSION] Re: [XEN PATCH v4 4/4] eclair: move function and macro properties outside ECLAIR

[Simone Ballarin]

On 26/02/24 16:44, Andrew Cooper wrote:
> On 02/02/2024 3:16 pm, Simone Ballarin wrote:
>> From: Maria Celeste Cesario <maria.celeste.cesario@bugseng.com>
>>
>> Function and macro properties contained in ECLAIR/call_properties.ecl are of
>> general interest: this patch moves these annotations in a generaric JSON file
>> in docs. In this way, they can be exploited for other purposes (i.e. documentation,
>> other tools).
>>
>> Add rst file containing explanation on how to update function_macro_properties.json.
>> Add script to convert the JSON file in ECL configurations.
>> Remove ECLAIR/call_properties.ecl: the file is now automatically generated from
>> the JSON file.
>>
>> Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>
>> Signed-off-by: Simone Ballarin  <simone.ballarin@bugseng.com>
>>
>> ---
>> Changes in v4:
>> - add missing script for converting the JSON file in ECL configurations;
>> - improve commit message;
>> - remove call_properties.ecs.
>> ---
>>   .../eclair_analysis/ECLAIR/analysis.ecl       |   1 +
>>   .../ECLAIR/call_properties.ecl                | 128 ---
>>   automation/eclair_analysis/prepare.sh         |   2 +
>>   automation/eclair_analysis/propertyparser.py  |  37 +
>>   docs/function_macro_properties.json           | 841 ++++++++++++++++++
>>   docs/function_macro_properties.rst            |  58 ++
>>   6 files changed, 939 insertions(+), 128 deletions(-)
>>   delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl
>>   create mode 100644 automation/eclair_analysis/propertyparser.py
>>   create mode 100644 docs/function_macro_properties.json
>>   create mode 100644 docs/function_macro_properties.rst
> 
> This breaks the Sphinx build.
> 
> checking consistency...
> /local/xen.git/docs/function_macro_properties.rst: WARNING: document
> isn't included in any toctree
> 
> Also, the top level of docs really isn't an appropriate place to put
> it.  Everything else is in docs/misra/.
> 
> When you've moved the files, you'll need to edit docs/misra/index.rst to
> fix the build.
> 
> ~Andrew
> 

I've submitted a new patch moving these files in docs/misra
and adding the rst file in the docs/misra/index.rst's toctree.

-- 
Simone Ballarin, M.Sc.

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