Re: Misra R17.1 in Xen

[Andrew Cooper <andrew.cooper3@xxxxxxxxxx>]

On 30/12/2025 6:28 pm, Nicola Vetrini wrote:
> On 2025-12-30 18:34, Nicola Vetrini wrote:
>> On 2025-12-30 18:05, Andrew Cooper wrote:
>>> Hello,
>>>
>>> The x86_64-allcode run highlights one new violation of R17.1,
>>> vmcoreinfo_append_str().  In writing this email, I've found another in
>>> debugtrace_printk() meaning that we're missing some options in the
>>> -allcode configuration.
>>>
>>> In deviations.ecl we have:
>>>
>>> -doc_begin="printf()-like functions are allowed to use the variadic
>>> features provided by stdarg.h."
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printk\\(.*\\)$)))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printf\\(.*\\)$)))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(panic)&&kind(function))))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(elf_call_log_callback)&&kind(function))))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(vprintk_common)&&kind(function))))"}
>>>
>>> -config=MC3A2.R17.1,macros+={hide , "^va_(arg|start|copy|end)$"}
>>> -doc_end
>>>
>>>
>>> First, we have no printf() so that row should be removed.
>>>
>>
>> I think it was for other variants of printf that are present in Xen
>> (e.g. vsnprintf). Perhaps it could be restricted a bit to be more
>> explicit.
>>
>>> But, more importantly this is safe if and only if the function
>>> declaration uses __attribute__((__format__(printf, ...))) to cause the
>>> compiler to perform format typechecking.
>>>
>>> Is it possible to encode this attribute requirement in the Eclair
>>> expression, so that e.g. accidentally dropping the attribute causes a
>>> violation to be reported?  This would also be rather safer than
>>> assuming
>>> that any prefix on printk() is safe.
>>>
>>
>> Well, the UBs associated to that rule (to varargs in general) go
>> beyond the formatting issues, but checking that the function decl has
>> the attribute is a good suggestion to harden these deviations. I'll
>> make some experiments and report back on this thread.
>
> Currently it is possible to match on the presence of the attribute
> "format", not on its arguments. Since "printf" is the only archetype
> used with "format" I don't think this is a big issue currently, but
> I'll let you be the judge on that.

There's scanf as the other option to format, but I suppose for the
specifics of a deviation for va_list, not being able to
match/distinguish format from scanf is fine.

~Andrew