Re: Misra R17.1 in Xen

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

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.

> Thanks,
> 
> ~Andrew

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