All of lore.kernel.org
 help / color / mirror / Atom feed
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


  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.