From: Nicola Vetrini <nicola.vetrini@bugseng.com>
To: Dmytro Prokopchuk1 <dmytro_prokopchuk1@epam.com>
Cc: xen-devel@lists.xenproject.org,
"Doug Goldstein" <cardoe@cardoe.com>,
"Stefano Stabellini" <sstabellini@kernel.org>,
"Andrew Cooper" <andrew.cooper3@citrix.com>,
"Anthony PERARD" <anthony.perard@vates.tech>,
"Michal Orzel" <michal.orzel@amd.com>,
"Jan Beulich" <jbeulich@suse.com>,
"Julien Grall" <julien@xen.org>,
"Roger Pau Monné" <roger@xenproject.org>
Subject: Re: [PATCH] automation/eclair: generalize the noreturn function-pointer deviation
Date: Fri, 09 Oct 2026 17:37:19 +0200 [thread overview]
Message-ID: <5b5cccc8bbbc4c87fc99427eb4c1c413@bugseng.com> (raw)
In-Reply-To: <d68c56607781bfa829766aed36eeb31f06080fbc.1791224638.git.dmytro_prokopchuk1@epam.com>
On 2026-10-05 20:56, Dmytro Prokopchuk1 wrote:
> The R11.1 safe cast only matched void noreturn (*)(void *). Accept any
> noreturn function pointer converted to a compatible function pointer.
> canonical() covers typeof destinations, and compatible_deep_unqualified
> keeps the parameter and return types aligned.
>
> Signed-off-by: Dmytro Prokopchuk <dmytro_prokopchuk1@epam.com>
> ---
>
> This patch tries to cover both of these:
>
> 1. eclair: widen R11.1 noreturn cast deviation
> https://patchew.org/Xen/c6632dd805a119aca54b9d1ae2eea68ef9c1334c.1790674358.git.dmytro._5Fprokopchuk1@epam.com/
>
> 2. Eclair: relax "noreturn" function-pointer conversion deviation
> https://patchew.org/Xen/6d212d60-5c0b-4909-996d-5d6a4906b7e1@suse.com/4cca58b6-b555-4064-aa26-5204dc4b99cc@suse.com/
>
> Test CI pipeline:
> https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/2914802667
>
> The only one Rule11.1 violation remains, which is covered by this Jan's
> patch:
> x86/kexec: address Misra rule 11.1 violation in machine_kexec_load()
>
The change itself is fine, but the aspect I'm concerned with is the
following: if you have a function marked noreturn, the compiler is
entitled to
essentially remove any code following it, so in principle this could be
the case also when invoking a function pointer (i.e. the compiler has no
obligation to retain code after a call to a function pointer that is
actually a noreturn function). While this in practice may not happen
often (e.g., the analysis done by a compiler is probably too shallow to
actually infer paths where the function pointer is only ever assigned to
noreturn functions when it is called), it is still not completely true
to say that the behavior is not altered by casting away noreturn. I have
given in [1] my R-by to the previous form of this deviation, but I
realize that this aspect should be mentioned. This is of course
supported by testing and code coverage evidence that the behavior is
indeed the same, or a suitable guarantee from the compiler vendor that
the behavior never diverges.
[1]
https://gitlab.com/xen-project/hardware/xen/-/commit/b5497ad4a4a2b9a97100ca002cc82b573b198071
> ---
> automation/eclair_analysis/ECLAIR/deviations.ecl | 9 +++++----
> docs/misra/deviations.rst | 8 ++++----
> docs/misra/rules.rst | 7 ++++---
> 3 files changed, 13 insertions(+), 11 deletions(-)
>
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl
> b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index 6cdb10a129..d89976a894 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -394,11 +394,12 @@ constant expressions are required.\""
> }
> -doc_end
>
> --doc_begin="The conversion from 'void noreturn (*)(void *)' to 'void
> (*)(void *)' is safe
> -because the semantics of the 'noreturn' attribute do not alter the
> calling convention or behavior of the resulting code."
> +-doc_begin="The conversion from a noreturn function pointer to a
> function pointer
> +with a compatible signature is safe because the semantics of the
> 'noreturn'
> +attribute do not alter the calling convention or behavior of the
> resulting code."
> -config=MC3A2.R11.1,casts+={safe,
> -
> "kind(bitcast)&&to(type(pointer(inner(return(builtin(void))&&all_param(1,
> pointer(builtin(void)))))))&&from(expr(skip(!syntactic(),
> - ref(property(noreturn)))))"}
> +
> "kind(bitcast)&&to(type(canonical(__function_pointer_types)))&&from(expr(skip(!syntactic(),
> + ref(property(noreturn)))))&&relation(compatible_deep_unqualified)"}
> -doc_end
>
> -doc_begin="The conversion from a pointer to an incomplete type to
> unsigned long does not lose any information, provided that the target
> type has enough bits to store it."
> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> index 6bcc2adf95..ed7129b8dc 100644
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -392,10 +392,10 @@ Deviations related to MISRA C:2012 Rules:
> - Tagged as `safe` for ECLAIR.
>
> * - R11.1
> - - The conversion from 'void noreturn (*)(...)' to 'void (*)(...)'
> is safe
> - because the semantics of the 'noreturn' attribute do not alter
> the calling
> - convention or behavior of the resulting code, parameters
> handling remain
> - consistent.
> + - The conversion from a noreturn function pointer to a function
> pointer
> + with a compatible signature is safe because the semantics of
> the
> + 'noreturn' attribute do not alter the calling convention or
> behavior
> + of the resulting code.
> - Tagged as `safe` for ECLAIR.
>
> * - R11.2
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index a59cf1782e..bd288bba29 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -435,9 +435,10 @@ maintainers if you want to suggest a change.
> and any other type
> - All conversions to integer types are permitted if the
> destination
> type has enough bits to hold the entire value. Conversions to
> bool
> - and void* are permitted. Conversions from 'void noreturn
> (*)(...)'
> - to 'void (*)(...)' are permitted. Conversions from [unsigned]
> long
> - or '(void *)' to a function pointer are permitted.
> + and void* are permitted. Conversions from a noreturn function
> pointer
> + to a function pointer with a compatible signature are
> permitted.
> + Conversions from [unsigned] long or '(void *)' to a function
> pointer
> + are permitted.
> Example::
>
> unsigned long func_addr = (unsigned long)&some_function;
--
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253
next prev parent reply other threads:[~2026-10-09 15:37 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-10-05 18:56 [PATCH] automation/eclair: generalize the noreturn function-pointer deviation Dmytro Prokopchuk1
2026-10-06 6:09 ` Jan Beulich
2026-10-09 15:37 ` Nicola Vetrini [this message]
2026-10-12 6:52 ` Jan Beulich
2026-10-13 7:29 ` Dmytro Prokopchuk1
2026-10-13 11:46 ` Nicola Vetrini
2026-10-13 12:37 ` Jan Beulich
2026-10-13 12:52 ` Nicola Vetrini
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=5b5cccc8bbbc4c87fc99427eb4c1c413@bugseng.com \
--to=nicola.vetrini@bugseng.com \
--cc=andrew.cooper3@citrix.com \
--cc=anthony.perard@vates.tech \
--cc=cardoe@cardoe.com \
--cc=dmytro_prokopchuk1@epam.com \
--cc=jbeulich@suse.com \
--cc=julien@xen.org \
--cc=michal.orzel@amd.com \
--cc=roger@xenproject.org \
--cc=sstabellini@kernel.org \
--cc=xen-devel@lists.xenproject.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.