Re: Misra R17.1 in Xen

[Nicola Vetrini <nicola.vetrini@bugseng.com>]

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.

> 
>> Thanks,
>> 
>> ~Andrew

-- 
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253