[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.2023 18:34, Simone Ballarin wrote: > 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. Let's assume we have a BUG_ON() (as the "crash effect") the condition of which depends on where in the sequence of operations it actually executes, i.e. (potentially) dependent upon another part of the initializer. I hope we agree that's not something that should be deviated? Yet even the re- worded statement would - according to my reading - permit doing so. I guess I should try to remember to bring this up on this afternoon's call. >>>>> --- 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. I'm afraid I don't see what would be constituting a violation here. Jan
|
Lists.xenproject.org is hosted with RackSpace, monitoring our |