.../eclair_analysis/ECLAIR/deviations.ecl | 12 ++++++++++++ docs/misra/deviations.rst | 17 +++++++++++++++++ 2 files changed, 29 insertions(+)
MISRA C Rule 2.1 states: "A project shall not contain unreachable code".
Functions that are non-returning and are not explicitly annotated with
the 'noreturn' attribute are considered a violation of this rule.
In certain cases, some functions might be non-returning in specific build
configurations due to call to '__builtin_unreachable()' in the expansion
of the macro 'BUG()':
- functions 'gicv3_do_LPI()' and 'gicv3_its_setup_collection()' when the
config CONFIG_HAS_ITS is not defined, it is intentionally used to catch
and prevent any unintended execution of code that should only run when
ITS is available;
- function 'prepare_acpi()' when the config CONFIG_ACPI is not defined,
to trigger an error if ACPI-related features are used incorrectly.
Although these functions are defined as 'static inline' and the compiler
may remove them from the object if they are not called (e.g., during Dead
Code Elimination (DCE)), they are still present after preprocessing and
are analyzed by the Eclair tool (regardless of whether this code is later
removed by the compiler). This is what causes Eclair to detect these rule
violations.
To account for that in specific builds, update the ECLAIR configuration
to deviate these violations. Update deviations.rst file accordingly.
No functional changes.
Signed-off-by: Dmytro Prokopchuk <dmytro_prokopchuk1@epam.com>
---
Changes in v2:
- updated commit message (added explanation why the Eclair detects these
violations)
- aligned Eclair configs with deviations wordings (explicit specify header
file and function 'static inline' attributes)
Link to v1:
https://patchew.org/Xen/f7b4112aad84162c25f96a9d6db43a0c2ba85daa.1756046023.git.dmytro._5Fprokopchuk1@epam.com/
Test CI pipeline:
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/2042397534
---
.../eclair_analysis/ECLAIR/deviations.ecl | 12 ++++++++++++
docs/misra/deviations.rst | 17 +++++++++++++++++
2 files changed, 29 insertions(+)
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 7f3fd35a33..c10dbf4f26 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -41,6 +41,18 @@ not executable, and therefore it is safe for them to be unreachable."
-call_properties+={"name(__builtin_unreachable)&&stmt(begin(any_exp(macro(name(ASSERT_UNREACHABLE)))))", {"noreturn(false)"}}
-doc_end
+-doc_begin="In the specific build configuration (when the config CONFIG_ACPI is not defined) the 'BUG()' macro is intentionally
+used in the 'prepare_acpi()' function defined as 'static inline' in the header file 'xen/arch/arm/include/asm/domain_build.h'
+to trigger a runtime error if ACPI-related features are used incorrectly."
+-config=MC3A2.R2.1,reports+={deliberate, "any_area(any_loc(file(^xen/arch/arm/include/asm/domain_build\\.h$))&&context(name(prepare_acpi)&&written_inline()&&written_storage(static)))"}
+-doc_end
+
+-doc_begin="In the specific build configuration (when the config CONFIG_HAS_ITS is not defined) the 'BUG()' macro is intentionally
+used in the 'gicv3_do_LPI()' and 'gicv3_its_setup_collection()' functions defined as 'static inline' in the header file 'xen/arch/arm/include/asm/gic_v3_its.h'
+to catch and prevent any unintended execution of code that should only run when ITS is available."
+-config=MC3A2.R2.1,reports+={deliberate, "any_area(any_loc(file(^xen/arch/arm/include/asm/gic_v3_its\\.h$))&&context(name(gicv3_do_LPI||gicv3_its_setup_collection)&&written_inline()&&written_storage(static)))"}
+-doc_end
+
-doc_begin="Proving compliance with respect to Rule 2.2 is generally impossible:
see https://arxiv.org/abs/2212.13933 for details. Moreover, peer review gives us
confidence that no evidence of errors in the program's logic has been missed due
diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
index 3271317206..45f665d5e3 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules:
even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed.
- ECLAIR has been configured to ignore those statements.
+ * - R2.1
+ - In the specific build configuration (when the config CONFIG_ACPI is not
+ defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()'
+ function in the header file 'xen/arch/arm/include/asm/domain_build.h'
+ defined as 'static inline' to trigger a runtime error if ACPI-related
+ features are used incorrectly.
+ - Tagged as `deliberate` for ECLAIR.
+
+ * - R2.1
+ - In the specific build configuration (when the config CONFIG_HAS_ITS is not
+ defined) the 'BUG()' macro is intentionally used in the 'gicv3_do_LPI()'
+ and 'gicv3_its_setup_collection()' functions defined as 'static inline'
+ in the header file 'xen/arch/arm/include/asm/gic_v3_its.h' to catch and
+ prevent any unintended execution of code that should only run when ITS is
+ available.
+ - Tagged as `deliberate` for ECLAIR.
+
* - R2.2
- Proving compliance with respect to Rule 2.2 is generally impossible:
see `<https://arxiv.org/abs/2212.13933>`_ for details. Moreover, peer
--
2.43.0
On 16.09.2025 14:45, Dmytro Prokopchuk1 wrote: > --- a/docs/misra/deviations.rst > +++ b/docs/misra/deviations.rst > @@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules: > even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed. > - ECLAIR has been configured to ignore those statements. > > + * - R2.1 > + - In the specific build configuration (when the config CONFIG_ACPI is not > + defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()' > + function in the header file 'xen/arch/arm/include/asm/domain_build.h' > + defined as 'static inline' to trigger a runtime error if ACPI-related > + features are used incorrectly. > + - Tagged as `deliberate` for ECLAIR. I response to me outlining a deviation-less alternative you tried it out and said it works. Then why is the deviation still being put in place? > + * - R2.1 > + - In the specific build configuration (when the config CONFIG_HAS_ITS is not > + defined) the 'BUG()' macro is intentionally used in the 'gicv3_do_LPI()' > + and 'gicv3_its_setup_collection()' functions defined as 'static inline' > + in the header file 'xen/arch/arm/include/asm/gic_v3_its.h' to catch and > + prevent any unintended execution of code that should only run when ITS is > + available. > + - Tagged as `deliberate` for ECLAIR. Taking both together and considering that really, when we no longer limit Misra checking to specific configurations, we are going to have many more of such "problems", I fear this way of deviating them simply doesn't scale. Imo this needs a SAF-style deviation that can be applied without needing to add a new section of text every time. Jan
On 9/16/25 17:27, Jan Beulich wrote:
> On 16.09.2025 14:45, Dmytro Prokopchuk1 wrote:
>> --- a/docs/misra/deviations.rst
>> +++ b/docs/misra/deviations.rst
>> @@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules:
>> even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed.
>> - ECLAIR has been configured to ignore those statements.
>>
>> + * - R2.1
>> + - In the specific build configuration (when the config CONFIG_ACPI is not
>> + defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()'
>> + function in the header file 'xen/arch/arm/include/asm/domain_build.h'
>> + defined as 'static inline' to trigger a runtime error if ACPI-related
>> + features are used incorrectly.
>> + - Tagged as `deliberate` for ECLAIR.
>
> I response to me outlining a deviation-less alternative you tried it out
> and said it works. Then why is the deviation still being put in place?
Yes, that's true.
I started with that prepare_acpi() function and I tried to move it into
xen/include/xen/acpi.h header file under appropriate #ifdef:
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/commit/d15cf91de92f1f8ec67911c51a13e7f095c1bcdd
The Eclair didn't report violations related to the prepare_acpi().
I was confused why Eclair continued to report other violations, and
didn't report for the prepare_acpi().
After a while I realized that this header file 'xen/include/xen/acpi.h'
was placed into exclude list 'docs/misra/exclude-list.json',
where:
{
"rel_path": "include/xen/acpi.h",
"comment": "Imported from Linux, ignore for now"
},
So, all violations from the 'include/xen/acpi.h' file were ignored.
It was just a coincidence.
>
>> + * - R2.1
>> + - In the specific build configuration (when the config CONFIG_HAS_ITS is not
>> + defined) the 'BUG()' macro is intentionally used in the 'gicv3_do_LPI()'
>> + and 'gicv3_its_setup_collection()' functions defined as 'static inline'
>> + in the header file 'xen/arch/arm/include/asm/gic_v3_its.h' to catch and
>> + prevent any unintended execution of code that should only run when ITS is
>> + available.
>> + - Tagged as `deliberate` for ECLAIR.
>
> Taking both together and considering that really, when we no longer limit
> Misra checking to specific configurations, we are going to have many more
> of such "problems", I fear this way of deviating them simply doesn't scale.
> Imo this needs a SAF-style deviation that can be applied without needing to
> add a new section of text every time.
>
> Jan
I agree. Actually, I saw similar functions. It could be tricky to
maintain Eclair configs.
I will create SAF-based patch.
Thanks,
Dmytro.
On 16.09.2025 21:35, Dmytro Prokopchuk1 wrote: > > > On 9/16/25 17:27, Jan Beulich wrote: >> On 16.09.2025 14:45, Dmytro Prokopchuk1 wrote: >>> --- a/docs/misra/deviations.rst >>> +++ b/docs/misra/deviations.rst >>> @@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules: >>> even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed. >>> - ECLAIR has been configured to ignore those statements. >>> >>> + * - R2.1 >>> + - In the specific build configuration (when the config CONFIG_ACPI is not >>> + defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()' >>> + function in the header file 'xen/arch/arm/include/asm/domain_build.h' >>> + defined as 'static inline' to trigger a runtime error if ACPI-related >>> + features are used incorrectly. >>> + - Tagged as `deliberate` for ECLAIR. >> >> I response to me outlining a deviation-less alternative you tried it out >> and said it works. Then why is the deviation still being put in place? > > Yes, that's true. > I started with that prepare_acpi() function and I tried to move it into > xen/include/xen/acpi.h header file under appropriate #ifdef: > https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/commit/d15cf91de92f1f8ec67911c51a13e7f095c1bcdd But an important part of my proposal was to have no #ifdef around the declaration, iirc. With that, no violation should result. Whether (or why) moving would be required I don't know. Jan
On 9/16/25 23:03, Jan Beulich wrote: > On 16.09.2025 21:35, Dmytro Prokopchuk1 wrote: >> >> >> On 9/16/25 17:27, Jan Beulich wrote: >>> On 16.09.2025 14:45, Dmytro Prokopchuk1 wrote: >>>> --- a/docs/misra/deviations.rst >>>> +++ b/docs/misra/deviations.rst >>>> @@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules: >>>> even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed. >>>> - ECLAIR has been configured to ignore those statements. >>>> >>>> + * - R2.1 >>>> + - In the specific build configuration (when the config CONFIG_ACPI is not >>>> + defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()' >>>> + function in the header file 'xen/arch/arm/include/asm/domain_build.h' >>>> + defined as 'static inline' to trigger a runtime error if ACPI-related >>>> + features are used incorrectly. >>>> + - Tagged as `deliberate` for ECLAIR. >>> >>> I response to me outlining a deviation-less alternative you tried it out >>> and said it works. Then why is the deviation still being put in place? >> >> Yes, that's true. >> I started with that prepare_acpi() function and I tried to move it into >> xen/include/xen/acpi.h header file under appropriate #ifdef: >> https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/commit/d15cf91de92f1f8ec67911c51a13e7f095c1bcdd > > But an important part of my proposal was to have no #ifdef around > the declaration, iirc. With that, no violation should result. I don't understand, how it can help to avoid scanning by the Eclair? In particular build configuration the "static inline" version of the function will be present after preproccesor, and Eclair will scan it. Jan, please, explain your thought. I think, I missed something. > Whether (or why) moving would be required I don't know. It shouldn't be moved. Nevermind.> > Jan Dmytro.
On 17.09.2025 15:59, Dmytro Prokopchuk1 wrote: > > > On 9/16/25 23:03, Jan Beulich wrote: >> On 16.09.2025 21:35, Dmytro Prokopchuk1 wrote: >>> >>> >>> On 9/16/25 17:27, Jan Beulich wrote: >>>> On 16.09.2025 14:45, Dmytro Prokopchuk1 wrote: >>>>> --- a/docs/misra/deviations.rst >>>>> +++ b/docs/misra/deviations.rst >>>>> @@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules: >>>>> even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed. >>>>> - ECLAIR has been configured to ignore those statements. >>>>> >>>>> + * - R2.1 >>>>> + - In the specific build configuration (when the config CONFIG_ACPI is not >>>>> + defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()' >>>>> + function in the header file 'xen/arch/arm/include/asm/domain_build.h' >>>>> + defined as 'static inline' to trigger a runtime error if ACPI-related >>>>> + features are used incorrectly. >>>>> + - Tagged as `deliberate` for ECLAIR. >>>> >>>> I response to me outlining a deviation-less alternative you tried it out >>>> and said it works. Then why is the deviation still being put in place? >>> >>> Yes, that's true. >>> I started with that prepare_acpi() function and I tried to move it into >>> xen/include/xen/acpi.h header file under appropriate #ifdef: >>> https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/commit/d15cf91de92f1f8ec67911c51a13e7f095c1bcdd >> >> But an important part of my proposal was to have no #ifdef around >> the declaration, iirc. With that, no violation should result. > I don't understand, how it can help to avoid scanning by the Eclair? I didn't say it would. Scanning will always happen. The question is whether Eclair would flag anything. > In particular build configuration the "static inline" version of the > function will be present after preproccesor, and Eclair will scan it. > > Jan, please, explain your thought. I think, I missed something. If acpi_disabled is compile-time-constant false, all you need is a declaration for prepare_acpi(). The call to it will then be DCE-ed. No inline function, no #ifdef, no violation. Jan
On 9/17/25 17:16, Jan Beulich wrote:
> On 17.09.2025 15:59, Dmytro Prokopchuk1 wrote:
>>
>>
>> On 9/16/25 23:03, Jan Beulich wrote:
>>> On 16.09.2025 21:35, Dmytro Prokopchuk1 wrote:
>>>>
>>>>
>>>> On 9/16/25 17:27, Jan Beulich wrote:
>>>>> On 16.09.2025 14:45, Dmytro Prokopchuk1 wrote:
>>>>>> --- a/docs/misra/deviations.rst
>>>>>> +++ b/docs/misra/deviations.rst
>>>>>> @@ -98,6 +98,23 @@ Deviations related to MISRA C:2012 Rules:
>>>>>> even when debug-only assertions like `ASSERT_UNREACHABLE()` are removed.
>>>>>> - ECLAIR has been configured to ignore those statements.
>>>>>>
>>>>>> + * - R2.1
>>>>>> + - In the specific build configuration (when the config CONFIG_ACPI is not
>>>>>> + defined) the 'BUG()' macro is intentionally used in the 'prepare_acpi()'
>>>>>> + function in the header file 'xen/arch/arm/include/asm/domain_build.h'
>>>>>> + defined as 'static inline' to trigger a runtime error if ACPI-related
>>>>>> + features are used incorrectly.
>>>>>> + - Tagged as `deliberate` for ECLAIR.
>>>>>
>>>>> I response to me outlining a deviation-less alternative you tried it out
>>>>> and said it works. Then why is the deviation still being put in place?
>>>>
>>>> Yes, that's true.
>>>> I started with that prepare_acpi() function and I tried to move it into
>>>> xen/include/xen/acpi.h header file under appropriate #ifdef:
>>>> https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/commit/d15cf91de92f1f8ec67911c51a13e7f095c1bcdd
>>>
>>> But an important part of my proposal was to have no #ifdef around
>>> the declaration, iirc. With that, no violation should result.
>> I don't understand, how it can help to avoid scanning by the Eclair?
>
> I didn't say it would. Scanning will always happen. The question is
> whether Eclair would flag anything.
>
>> In particular build configuration the "static inline" version of the
>> function will be present after preproccesor, and Eclair will scan it.
>>
>> Jan, please, explain your thought. I think, I missed something.
>
> If acpi_disabled is compile-time-constant false, all you need is a
> declaration for prepare_acpi(). The call to it will then be DCE-ed.
> No inline function, no #ifdef, no violation.
>
> Jan
Yeah... The key words were "No inline function". Now it's clear to me.
And it works fine for the 'prepare_acpi()' and
'gicv3_its_setup_collection()' functions.
No inline functions -> no violations. The Eclair is happy.
Instead of runtime checking we've got compile-time checking of the
functions invalid usage. Original idea is preserved.
Unfortunately, the function 'gicv3_do_LPI()' doesn't have a
compile-time-constant guard around it. Furthermore, it's assigned to the
callback pointer:
.do_LPI = gicv3_do_LPI,
It's possible to remove inline variant of this function,
put the following code inside #ifdef
#ifdef CONFIG_HAS_ITS
.do_LPI = gicv3_do_LPI,
#endif
and check callback pointer later
if ( gic_hw_ops->do_LPI )
gic_hw_ops->do_LPI(irq);
But we will lost the original idea (I mean having checking mechanism:
runtime or compile-time).
If you have some ideas, please let me know.
Otherwise, SAF comment should be created there.
Thanks,
Dmytro.
© 2016 - 2025 Red Hat, Inc.