Re: Misra R17.1 in Xen

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

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