Re: [PATCH] automation/eclair: generalize the noreturn function-pointer deviation

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

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@xxxxxxxx>
> ---
>
> 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@xxxxxxxx/
>
> 2. Eclair: relax "noreturn" function-pointer conversion deviation
> https://patchew.org/Xen/6d212d60-5c0b-4909-996d-5d6a4906b7e1@xxxxxxxx/4cca58b6-b555-4064-aa26-5204dc4b99cc@xxxxxxxx/
>
> 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