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
