[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [XEN PATCH v2 2/3] xen/arm: add SAF deviation for debugging and logging effects



On 27/11/23 16:09, Jan Beulich wrote:
On 27.11.2023 15:35, Simone Ballarin wrote:
On 27/11/23 11:46, Jan Beulich wrote:
On 24.11.2023 18:29, Simone Ballarin wrote:
--- 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."
+        },

I'm wary of this statement. Order may not matter much anymore _after_ an
abnormal condition was encountered, but in the course of determining whether
an abnormal condition might have been reached it may very well still matter.

Do you object to the deviation in general? Or just to the wording?

Primarily the wording. Yet the need to adjust the wording also hints at there
needing to be care when actually making use of this deviation. Which it turn
I'm not convinced is in the spirit of Misra

The rule is really strict, but imho the only real dangerous situation is
when an entry performs a persistent side effect that can change the
behavior of another entry. I.e.:

int y = 0;
int x[2] =
{
  y=1, /* first element will be always 1 */
  y    /* second element can be either 0 or 1 */
};

Above we have a dependency between the first entry and the second.

Now let's consider logging effects:

#define LOG(x) printf("LOG: %s", x);

int x[2] =
{
  ({ LOG("1"); 1; }),
  ({ LOG("2"); 2; })
};


Here the execution can print:
"LOG: 1LOG: 2" or
"LOG: 2LOG: 1".

Do we agree that the evaluation order of prints caused by logging
functions/macros do not normally cause dependencies between the
entries? The execution is still non-deterministic, but does it really
matter?.

In the case of function that crash execution, no dependencies can exist
since no further entries will be evaluated.

In conclusion, I propose the following rewording:

"text": "Effects that crash execution or produce logs are allowed in initializer lists. Logging effects do not affect the evaluation of subsequent entries. Crash effects are allowed as they represent the
end of the execution.



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

What's the debugging / logging reason on the commented line?

The "ASSERT(dev != NULL)" in its body.

"it" == device_get_class() I assume? Imo to unobvious to deal with like this.


Yes, Julien suggested to simply remove the ASSERT as it isn't really useful. I forgot his suggestion. In v3 I will remove it as suggested.

--- a/xen/arch/arm/guestcopy.c
+++ b/xen/arch/arm/guestcopy.c
@@ -110,18 +110,21 @@ 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,
+                      /* 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)
   {
+    /* SAF-4-safe No persistent side effects */
       return copy_guest((void *)from, (vaddr_t)to, len, GVA_INFO(current),
                         COPY_to_guest | COPY_flush_dcache | COPY_linear);
   }
unsigned long raw_clear_guest(void *to, unsigned int len)
   {
+    /* SAF-4-safe No persistent side effects */
       return copy_guest(NULL, (vaddr_t)to, len, GVA_INFO(current),
                         COPY_to_guest | COPY_linear);
   }
@@ -129,6 +132,7 @@ unsigned long raw_clear_guest(void *to, unsigned int len)
   unsigned long raw_copy_from_guest(void *to, const void __user *from,
                                     unsigned int len)
   {
+    /* SAF-4-safe No persistent side effects */
       return copy_guest(to, (vaddr_t)from, len, GVA_INFO(current),
                         COPY_from_guest | COPY_linear);
   }

I can only guess that in all four of these it's the use of "current" which
requires the comment. Yet imo that either needs making explicit, or such a
comment shouldn't go on use sites of "current", but on its definition site.


"current" does not contain any violation of R13.1. Its expansion
produces a side-effect, but this is not a problem in itself. The real
problem is that GVA_INFO expands it in an initializer list:
#define GVA_INFO(vcpu) ((copy_info_t) { .gva = { vcpu } })

But an initializer list doesn't itself constitute a side effect, does it?


The side effect should be inside the initializer list. { .gva = 1 } is not a violation.

GVA_INFO(current) is the real piece of code that requires to be
deviated.

In which case I think this such want spelling

     return copy_guest(to, (vaddr_t)from, len,
                       /* SAF-4-safe No persistent side effects */
                       GVA_INFO(current),
                       COPY_from_guest | COPY_linear);

or some such. Not the least because we want to make sure a deviation does
not have wider than necessary scope (which when formatted as above is,
aiui, always the following source line).


Yes, I agree.

Jan

--
Simone Ballarin, M.Sc.

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




 


Rackspace

Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.