automation/eclair_analysis/ECLAIR/deviations.ecl | 11 +++++++++++ docs/misra/deviations.rst | 13 +++++++++++++ 2 files changed, 24 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.
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>
---
Test CI pipeline:
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/2000738682
---
automation/eclair_analysis/ECLAIR/deviations.ecl | 11 +++++++++++
docs/misra/deviations.rst | 13 +++++++++++++
2 files changed, 24 insertions(+)
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 7f3fd35a33..336aec58c2 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -41,6 +41,17 @@ 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="The 'BUG()' macro is intentionally used in the 'prepare_acpi()' function in specific build configuration
+(when the config CONFIG_ACPI is not defined) to trigger an 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)))"}
+-doc_end
+
+-doc_begin="The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and 'gicv3_its_setup_collection()' functions
+in specific build configuration (when the config CONFIG_HAS_ITS is not defined) 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)))"}
+-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 2119066531..96eb202502 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
Xen expects developers to ensure code remains safe and reliable in builds,
even when debug-only assertions like `ASSERT_UNREACHABLE() are removed.
+ * - R2.1
+ - The 'BUG()' macro is intentionally used in the 'prepare_acpi()' function
+ in specific build configuration (when the config CONFIG_ACPI is not
+ defined) to trigger an error if ACPI-related features are used incorrectly.
+ - Tagged as `deliberate` for ECLAIR.
+
+ * - R2.1
+ - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
+ 'gicv3_its_setup_collection()' functions in specific build configuration
+ (when the config CONFIG_HAS_ITS is not defined) 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.0On 24.08.2025 16:56, Dmytro Prokopchuk1 wrote: > --- a/docs/misra/deviations.rst > +++ b/docs/misra/deviations.rst > @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules: > Xen expects developers to ensure code remains safe and reliable in builds, > even when debug-only assertions like `ASSERT_UNREACHABLE() are removed. > > + * - R2.1 > + - The 'BUG()' macro is intentionally used in the 'prepare_acpi()' function > + in specific build configuration (when the config CONFIG_ACPI is not > + defined) to trigger an error if ACPI-related features are used incorrectly. > + - Tagged as `deliberate` for ECLAIR. With #define acpi_disabled true in xen/acpi.h I don't see why we even have that inline stub. When it's dropped and the declaration left in place without #ifdef CONFIG_ACPI around it, the compiler will DCE the code (much like we arrange for in many other places). No deviation needed then. If such a deviation was to be added, it would need disambiguating. A function of the given name could appear in x86 as well. That wouldn't be covered by the Eclair config then, but it would be covered by the text here. > + * - R2.1 > + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and > + 'gicv3_its_setup_collection()' functions in specific build configuration > + (when the config CONFIG_HAS_ITS is not defined) to catch and prevent any > + unintended execution of code that should only run when ITS is available. > + - Tagged as `deliberate` for ECLAIR. I didn't look at this, but I would very much hope that something similar could be done there as well. Jan
On 8/25/25 13:07, Jan Beulich wrote:
> On 24.08.2025 16:56, Dmytro Prokopchuk1 wrote:
>> --- a/docs/misra/deviations.rst
>> +++ b/docs/misra/deviations.rst
>> @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
>> Xen expects developers to ensure code remains safe and reliable in builds,
>> even when debug-only assertions like `ASSERT_UNREACHABLE() are removed.
>>
>> + * - R2.1
>> + - The 'BUG()' macro is intentionally used in the 'prepare_acpi()' function
>> + in specific build configuration (when the config CONFIG_ACPI is not
>> + defined) to trigger an error if ACPI-related features are used incorrectly.
>> + - Tagged as `deliberate` for ECLAIR.
>
> With
>
> #define acpi_disabled true
>
> in xen/acpi.h I don't see why we even have that inline stub. When it's dropped
> and the declaration left in place without #ifdef CONFIG_ACPI around it, the
> compiler will DCE the code (much like we arrange for in many other places). No
> deviation needed then.
>
> If such a deviation was to be added, it would need disambiguating. A function
> of the given name could appear in x86 as well. That wouldn't be covered by the
> Eclair config then, but it would be covered by the text here.
>
>> + * - R2.1
>> + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
>> + 'gicv3_its_setup_collection()' functions in specific build configuration
>> + (when the config CONFIG_HAS_ITS is not defined) to catch and prevent any
>> + unintended execution of code that should only run when ITS is available.
>> + - Tagged as `deliberate` for ECLAIR.
>
> I didn't look at this, but I would very much hope that something similar could
> be done there as well.
>
> Jan
After small changes related to prepare_acpi() function, Misra R2.1
violation has gone. The compiler really does DCE:
if ( acpi_disabled <<< this is TRUE )
{
rc = prepare_dtb_hwdom(d, kinfo);
if ( rc < 0 )
return rc;
#ifdef CONFIG_HAS_PCI
rc = pci_host_bridge_mappings(d);
#endif
}
else
rc = prepare_acpi(d, kinfo); <<< DCE
I will publish it as separate patch.
Thanks to Jan, I really appreciate his help.
The situation with functions gicv3_do_LPI(),
gicv3_its_setup_collection() and config CONFIG_HAS_ITS is little bit
different.
The compiler can do DCE in case when config CONFIG_HAS_ITS is "y", and
Misra R2.1 violation related to these functions also can be resolved.
Actually, no changes in source code need for that.
But Eclair detects these violations because config CONFIG_HAS_ITS is
"n", and source code is really compiled with inline stub functions (with
BUG() macro).
This is because config CONFIG_HAS_ITS is "experimental/unsupported"
config HAS_ITS
bool "GICv3 ITS MSI controller support (UNSUPPORTED)" if
UNSUPPORTED
depends on GICV3 && !NEW_VGIC && !ARM_32
and to enable it need to set additional config: "CONFIG_UNSUPPORTED=y".
I tried to test it (added "CONFIG_UNSUPPORTED=y" into
automation/gitlab-ci/analyze.yaml file). You can see my CI pipeline:
https://eclair-analysis-logs.xenproject.org/fs/var/local/eclair/xen-project.ecdf/xen-project/people/dimaprkp4k/xen/ECLAIR_normal/rule_2.1_gicv3_its_host_has_its_v2/ARM64/11144854092/PROJECT.ecd;/by_service.html#service&kind
Unfortunately, I observed +6 new violations with that additional config
"CONFIG_UNSUPPORTED=y".
I don't know how and why these EXTRA_XEN_CONFIG were selected in the
file 'automation/gitlab-ci/analyze.yaml'. And are we able to add new
configs here ?....
So, I see the next plan (just from my point of view):
1. Add "CONFIG_UNSUPPORTED=y" and resolve new violations.
2. Continue with proposed deviation
3. ... ?
Thank you in advance.
Dmytro.
On 26.08.2025 20:07, Dmytro Prokopchuk1 wrote: > The situation with functions gicv3_do_LPI(), > gicv3_its_setup_collection() and config CONFIG_HAS_ITS is little bit > different. > The compiler can do DCE in case when config CONFIG_HAS_ITS is "y", and > Misra R2.1 violation related to these functions also can be resolved. > Actually, no changes in source code need for that. > But Eclair detects these violations because config CONFIG_HAS_ITS is > "n", and source code is really compiled with inline stub functions (with > BUG() macro). > This is because config CONFIG_HAS_ITS is "experimental/unsupported" > > config HAS_ITS > bool "GICv3 ITS MSI controller support (UNSUPPORTED)" if > UNSUPPORTED > depends on GICV3 && !NEW_VGIC && !ARM_32 > > and to enable it need to set additional config: "CONFIG_UNSUPPORTED=y". > > I tried to test it (added "CONFIG_UNSUPPORTED=y" into > automation/gitlab-ci/analyze.yaml file). You can see my CI pipeline: > https://eclair-analysis-logs.xenproject.org/fs/var/local/eclair/xen-project.ecdf/xen-project/people/dimaprkp4k/xen/ECLAIR_normal/rule_2.1_gicv3_its_host_has_its_v2/ARM64/11144854092/PROJECT.ecd;/by_service.html#service&kind > > Unfortunately, I observed +6 new violations with that additional config > "CONFIG_UNSUPPORTED=y". > > I don't know how and why these EXTRA_XEN_CONFIG were selected in the > file 'automation/gitlab-ci/analyze.yaml'. And are we able to add new > configs here ?.... This has been a repeated source for discussion. The present selection, afaict, is pretty arbitrary. However, in your considerations on how to address an issue, imo you should not look at the present config. Whatever the solution would better fit all possible settings. Jan
On 2025-08-26 20:07, Dmytro Prokopchuk1 wrote:
> On 8/25/25 13:07, Jan Beulich wrote:
>> On 24.08.2025 16:56, Dmytro Prokopchuk1 wrote:
>>> --- a/docs/misra/deviations.rst
>>> +++ b/docs/misra/deviations.rst
>>> @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
>>> Xen expects developers to ensure code remains safe and
>>> reliable in builds,
>>> even when debug-only assertions like `ASSERT_UNREACHABLE()
>>> are removed.
>>>
>>> + * - R2.1
>>> + - The 'BUG()' macro is intentionally used in the
>>> 'prepare_acpi()' function
>>> + in specific build configuration (when the config CONFIG_ACPI
>>> is not
>>> + defined) to trigger an error if ACPI-related features are
>>> used incorrectly.
>>> + - Tagged as `deliberate` for ECLAIR.
>>
>> With
>>
>> #define acpi_disabled true
>>
>> in xen/acpi.h I don't see why we even have that inline stub. When it's
>> dropped
>> and the declaration left in place without #ifdef CONFIG_ACPI around
>> it, the
>> compiler will DCE the code (much like we arrange for in many other
>> places). No
>> deviation needed then.
>>
>> If such a deviation was to be added, it would need disambiguating. A
>> function
>> of the given name could appear in x86 as well. That wouldn't be
>> covered by the
>> Eclair config then, but it would be covered by the text here.
>>
>>> + * - R2.1
>>> + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'()
>>> and
>>> + 'gicv3_its_setup_collection()' functions in specific build
>>> configuration
>>> + (when the config CONFIG_HAS_ITS is not defined) to catch and
>>> prevent any
>>> + unintended execution of code that should only run when ITS is
>>> available.
>>> + - Tagged as `deliberate` for ECLAIR.
>>
>> I didn't look at this, but I would very much hope that something
>> similar could
>> be done there as well.
>>
>> Jan
>
> After small changes related to prepare_acpi() function, Misra R2.1
> violation has gone. The compiler really does DCE:
>
> if ( acpi_disabled <<< this is TRUE )
> {
> rc = prepare_dtb_hwdom(d, kinfo);
> if ( rc < 0 )
> return rc;
> #ifdef CONFIG_HAS_PCI
> rc = pci_host_bridge_mappings(d);
> #endif
> }
> else
> rc = prepare_acpi(d, kinfo); <<< DCE
>
> I will publish it as separate patch.
> Thanks to Jan, I really appreciate his help.
>
>
> The situation with functions gicv3_do_LPI(),
> gicv3_its_setup_collection() and config CONFIG_HAS_ITS is little bit
> different.
> The compiler can do DCE in case when config CONFIG_HAS_ITS is "y", and
> Misra R2.1 violation related to these functions also can be resolved.
> Actually, no changes in source code need for that.
> But Eclair detects these violations because config CONFIG_HAS_ITS is
> "n", and source code is really compiled with inline stub functions
> (with
> BUG() macro).
> This is because config CONFIG_HAS_ITS is "experimental/unsupported"
>
> config HAS_ITS
> bool "GICv3 ITS MSI controller support (UNSUPPORTED)" if
> UNSUPPORTED
> depends on GICV3 && !NEW_VGIC && !ARM_32
>
> and to enable it need to set additional config: "CONFIG_UNSUPPORTED=y".
>
> I tried to test it (added "CONFIG_UNSUPPORTED=y" into
> automation/gitlab-ci/analyze.yaml file). You can see my CI pipeline:
> https://eclair-analysis-logs.xenproject.org/fs/var/local/eclair/xen-project.ecdf/xen-project/people/dimaprkp4k/xen/ECLAIR_normal/rule_2.1_gicv3_its_host_has_its_v2/ARM64/11144854092/PROJECT.ecd;/by_service.html#service&kind
>
> Unfortunately, I observed +6 new violations with that additional config
> "CONFIG_UNSUPPORTED=y".
>
> I don't know how and why these EXTRA_XEN_CONFIG were selected in the
> file 'automation/gitlab-ci/analyze.yaml'. And are we able to add new
> configs here ?....
>
You'll have to ask Stefano about that, but I doubt at this stage. Those
set of configs for Arm and X86 has been selected ~2 years ago.
> So, I see the next plan (just from my point of view):
> 1. Add "CONFIG_UNSUPPORTED=y" and resolve new violations.
> 2. Continue with proposed deviation
> 3. ... ?
>
> Thank you in advance.
> Dmytro.
--
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253
On Tue, 26 Aug 2025, Nicola Vetrini wrote:
> On 2025-08-26 20:07, Dmytro Prokopchuk1 wrote:
> > On 8/25/25 13:07, Jan Beulich wrote:
> > > On 24.08.2025 16:56, Dmytro Prokopchuk1 wrote:
> > > > --- a/docs/misra/deviations.rst
> > > > +++ b/docs/misra/deviations.rst
> > > > @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
> > > > Xen expects developers to ensure code remains safe and reliable
> > > > in builds,
> > > > even when debug-only assertions like `ASSERT_UNREACHABLE() are
> > > > removed.
> > > >
> > > > + * - R2.1
> > > > + - The 'BUG()' macro is intentionally used in the 'prepare_acpi()'
> > > > function
> > > > + in specific build configuration (when the config CONFIG_ACPI is
> > > > not
> > > > + defined) to trigger an error if ACPI-related features are used
> > > > incorrectly.
> > > > + - Tagged as `deliberate` for ECLAIR.
> > >
> > > With
> > >
> > > #define acpi_disabled true
> > >
> > > in xen/acpi.h I don't see why we even have that inline stub. When it's
> > > dropped
> > > and the declaration left in place without #ifdef CONFIG_ACPI around it,
> > > the
> > > compiler will DCE the code (much like we arrange for in many other
> > > places). No
> > > deviation needed then.
> > >
> > > If such a deviation was to be added, it would need disambiguating. A
> > > function
> > > of the given name could appear in x86 as well. That wouldn't be covered by
> > > the
> > > Eclair config then, but it would be covered by the text here.
> > >
> > > > + * - R2.1
> > > > + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
> > > > + 'gicv3_its_setup_collection()' functions in specific build
> > > > configuration
> > > > + (when the config CONFIG_HAS_ITS is not defined) to catch and
> > > > prevent any
> > > > + unintended execution of code that should only run when ITS is
> > > > available.
> > > > + - Tagged as `deliberate` for ECLAIR.
> > >
> > > I didn't look at this, but I would very much hope that something similar
> > > could
> > > be done there as well.
> > >
> > > Jan
> >
> > After small changes related to prepare_acpi() function, Misra R2.1
> > violation has gone. The compiler really does DCE:
> >
> > if ( acpi_disabled <<< this is TRUE )
> > {
> > rc = prepare_dtb_hwdom(d, kinfo);
> > if ( rc < 0 )
> > return rc;
> > #ifdef CONFIG_HAS_PCI
> > rc = pci_host_bridge_mappings(d);
> > #endif
> > }
> > else
> > rc = prepare_acpi(d, kinfo); <<< DCE
> >
> > I will publish it as separate patch.
> > Thanks to Jan, I really appreciate his help.
> >
> >
> > The situation with functions gicv3_do_LPI(),
> > gicv3_its_setup_collection() and config CONFIG_HAS_ITS is little bit
> > different.
> > The compiler can do DCE in case when config CONFIG_HAS_ITS is "y", and
> > Misra R2.1 violation related to these functions also can be resolved.
> > Actually, no changes in source code need for that.
> > But Eclair detects these violations because config CONFIG_HAS_ITS is
> > "n", and source code is really compiled with inline stub functions (with
> > BUG() macro).
> > This is because config CONFIG_HAS_ITS is "experimental/unsupported"
> >
> > config HAS_ITS
> > bool "GICv3 ITS MSI controller support (UNSUPPORTED)" if
> > UNSUPPORTED
> > depends on GICV3 && !NEW_VGIC && !ARM_32
> >
> > and to enable it need to set additional config: "CONFIG_UNSUPPORTED=y".
> >
> > I tried to test it (added "CONFIG_UNSUPPORTED=y" into
> > automation/gitlab-ci/analyze.yaml file). You can see my CI pipeline:
> > https://eclair-analysis-logs.xenproject.org/fs/var/local/eclair/xen-project.ecdf/xen-project/people/dimaprkp4k/xen/ECLAIR_normal/rule_2.1_gicv3_its_host_has_its_v2/ARM64/11144854092/PROJECT.ecd;/by_service.html#service&kind
> >
> > Unfortunately, I observed +6 new violations with that additional config
> > "CONFIG_UNSUPPORTED=y".
> >
> > I don't know how and why these EXTRA_XEN_CONFIG were selected in the
> > file 'automation/gitlab-ci/analyze.yaml'. And are we able to add new
> > configs here ?....
> >
>
> You'll have to ask Stefano about that, but I doubt at this stage. Those set of
> configs for Arm and X86 has been selected ~2 years ago.
We have migrated to a new faster ECLAIR runner.
I do not think we should change the existing configuration. If anything,
I would remove options from it rather than add more.
However, we can add additional configurations by creating more ECLAIR
jobs, and thanks to the new runner we should be able to keep up.
On 8/27/25 02:51, Stefano Stabellini wrote:
> On Tue, 26 Aug 2025, Nicola Vetrini wrote:
>> On 2025-08-26 20:07, Dmytro Prokopchuk1 wrote:
>>> On 8/25/25 13:07, Jan Beulich wrote:
>>>> On 24.08.2025 16:56, Dmytro Prokopchuk1 wrote:
>>>>> --- a/docs/misra/deviations.rst
>>>>> +++ b/docs/misra/deviations.rst
>>>>> @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
>>>>> Xen expects developers to ensure code remains safe and reliable
>>>>> in builds,
>>>>> even when debug-only assertions like `ASSERT_UNREACHABLE() are
>>>>> removed.
>>>>>
>>>>> + * - R2.1
>>>>> + - The 'BUG()' macro is intentionally used in the 'prepare_acpi()'
>>>>> function
>>>>> + in specific build configuration (when the config CONFIG_ACPI is
>>>>> not
>>>>> + defined) to trigger an error if ACPI-related features are used
>>>>> incorrectly.
>>>>> + - Tagged as `deliberate` for ECLAIR.
>>>>
>>>> With
>>>>
>>>> #define acpi_disabled true
>>>>
>>>> in xen/acpi.h I don't see why we even have that inline stub. When it's
>>>> dropped
>>>> and the declaration left in place without #ifdef CONFIG_ACPI around it,
>>>> the
>>>> compiler will DCE the code (much like we arrange for in many other
>>>> places). No
>>>> deviation needed then.
>>>>
>>>> If such a deviation was to be added, it would need disambiguating. A
>>>> function
>>>> of the given name could appear in x86 as well. That wouldn't be covered by
>>>> the
>>>> Eclair config then, but it would be covered by the text here.
>>>>
>>>>> + * - R2.1
>>>>> + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
>>>>> + 'gicv3_its_setup_collection()' functions in specific build
>>>>> configuration
>>>>> + (when the config CONFIG_HAS_ITS is not defined) to catch and
>>>>> prevent any
>>>>> + unintended execution of code that should only run when ITS is
>>>>> available.
>>>>> + - Tagged as `deliberate` for ECLAIR.
>>>>
>>>> I didn't look at this, but I would very much hope that something similar
>>>> could
>>>> be done there as well.
>>>>
>>>> Jan
>>>
>>> After small changes related to prepare_acpi() function, Misra R2.1
>>> violation has gone. The compiler really does DCE:
>>>
>>> if ( acpi_disabled <<< this is TRUE )
>>> {
>>> rc = prepare_dtb_hwdom(d, kinfo);
>>> if ( rc < 0 )
>>> return rc;
>>> #ifdef CONFIG_HAS_PCI
>>> rc = pci_host_bridge_mappings(d);
>>> #endif
>>> }
>>> else
>>> rc = prepare_acpi(d, kinfo); <<< DCE
>>>
>>> I will publish it as separate patch.
>>> Thanks to Jan, I really appreciate his help.
>>>
>>>
>>> The situation with functions gicv3_do_LPI(),
>>> gicv3_its_setup_collection() and config CONFIG_HAS_ITS is little bit
>>> different.
>>> The compiler can do DCE in case when config CONFIG_HAS_ITS is "y", and
>>> Misra R2.1 violation related to these functions also can be resolved.
>>> Actually, no changes in source code need for that.
>>> But Eclair detects these violations because config CONFIG_HAS_ITS is
>>> "n", and source code is really compiled with inline stub functions (with
>>> BUG() macro).
>>> This is because config CONFIG_HAS_ITS is "experimental/unsupported"
>>>
>>> config HAS_ITS
>>> bool "GICv3 ITS MSI controller support (UNSUPPORTED)" if
>>> UNSUPPORTED
>>> depends on GICV3 && !NEW_VGIC && !ARM_32
>>>
>>> and to enable it need to set additional config: "CONFIG_UNSUPPORTED=y".
>>>
>>> I tried to test it (added "CONFIG_UNSUPPORTED=y" into
>>> automation/gitlab-ci/analyze.yaml file). You can see my CI pipeline:
>>> https://eclair-analysis-logs.xenproject.org/fs/var/local/eclair/xen-project.ecdf/xen-project/people/dimaprkp4k/xen/ECLAIR_normal/rule_2.1_gicv3_its_host_has_its_v2/ARM64/11144854092/PROJECT.ecd;/by_service.html#service&kind
>>>
>>> Unfortunately, I observed +6 new violations with that additional config
>>> "CONFIG_UNSUPPORTED=y".
>>>
>>> I don't know how and why these EXTRA_XEN_CONFIG were selected in the
>>> file 'automation/gitlab-ci/analyze.yaml'. And are we able to add new
>>> configs here ?....
>>>
>>
>> You'll have to ask Stefano about that, but I doubt at this stage. Those set of
>> configs for Arm and X86 has been selected ~2 years ago.
>
> We have migrated to a new faster ECLAIR runner.
>
> I do not think we should change the existing configuration. If anything,
> I would remove options from it rather than add more.
>
> However, we can add additional configurations by creating more ECLAIR
> jobs, and thanks to the new runner we should be able to keep up.
I just realized, that the compiler should do DCE for
gicv3_its_setup_collection() in case of config CONFIG_HAS_ITS is "n".
if ( gicv3_its_host_has_its() <<< this is FALSE )
{
if ( !gicv3_enable_lpis() )
return -EBUSY;
ret = gicv3_its_setup_collection(smp_processor_id());
if ( ret )
return ret;
}
I'll take a look again.
On 8/25/25 13:07, Jan Beulich wrote: > On 24.08.2025 16:56, Dmytro Prokopchuk1 wrote: >> --- a/docs/misra/deviations.rst >> +++ b/docs/misra/deviations.rst >> @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules: >> Xen expects developers to ensure code remains safe and reliable in builds, >> even when debug-only assertions like `ASSERT_UNREACHABLE() are removed. >> >> + * - R2.1 >> + - The 'BUG()' macro is intentionally used in the 'prepare_acpi()' function >> + in specific build configuration (when the config CONFIG_ACPI is not >> + defined) to trigger an error if ACPI-related features are used incorrectly. >> + - Tagged as `deliberate` for ECLAIR. > > With > > #define acpi_disabled true > > in xen/acpi.h I don't see why we even have that inline stub. When it's dropped > and the declaration left in place without #ifdef CONFIG_ACPI around it, the > compiler will DCE the code (much like we arrange for in many other places). No > deviation needed then. > > If such a deviation was to be added, it would need disambiguating. A function > of the given name could appear in x86 as well. That wouldn't be covered by the > Eclair config then, but it would be covered by the text here. > >> + * - R2.1 >> + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and >> + 'gicv3_its_setup_collection()' functions in specific build configuration >> + (when the config CONFIG_HAS_ITS is not defined) to catch and prevent any >> + unintended execution of code that should only run when ITS is available. >> + - Tagged as `deliberate` for ECLAIR. > > I didn't look at this, but I would very much hope that something similar could > be done there as well. > > Jan Thank you for review, Jan. I'll pay attention on it. Dmytro.
On 2025-08-24 16:56, Dmytro Prokopchuk1 wrote:
> 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.
>
> 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>
> ---
> Test CI pipeline:
> https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/2000738682
> ---
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/jobs/11119212994
Build failure here
> automation/eclair_analysis/ECLAIR/deviations.ecl | 11 +++++++++++
> docs/misra/deviations.rst | 13 +++++++++++++
> 2 files changed, 24 insertions(+)
>
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl
> b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index 7f3fd35a33..336aec58c2 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -41,6 +41,17 @@ 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="The 'BUG()' macro is intentionally used in the
> 'prepare_acpi()' function in specific build configuration
> +(when the config CONFIG_ACPI is not defined) to trigger an 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)))"}
> +-doc_end
> +
> +-doc_begin="The 'BUG()' macro is intentionally used in
> 'gicv3_do_LPI'() and 'gicv3_its_setup_collection()' functions
> +in specific build configuration (when the config CONFIG_HAS_ITS is not
> defined) 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)))"}
> +-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 2119066531..96eb202502 100644
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
> Xen expects developers to ensure code remains safe and reliable
> in builds,
> even when debug-only assertions like `ASSERT_UNREACHABLE() are
> removed.
>
> + * - R2.1
> + - The 'BUG()' macro is intentionally used in the 'prepare_acpi()'
> function
> + in specific build configuration (when the config CONFIG_ACPI is
> not
> + defined) to trigger an error if ACPI-related features are used
> incorrectly.
> + - Tagged as `deliberate` for ECLAIR.
> +
> + * - R2.1
> + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
> + 'gicv3_its_setup_collection()' functions in specific build
> configuration
> + (when the config CONFIG_HAS_ITS is not defined) 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
--
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253
On 8/24/25 18:29, Nicola Vetrini wrote:
> On 2025-08-24 16:56, Dmytro Prokopchuk1 wrote:
>> 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.
>>
>> 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>
>> ---
>> Test CI pipeline:
>> https://eur01.safelinks.protection.outlook.com/?
>> url=https%3A%2F%2Fgitlab.com%2Fxen-
>> project%2Fpeople%2Fdimaprkp4k%2Fxen%2F-
>> %2Fpipelines%2F2000738682&data=05%7C02%7Cdmytro_prokopchuk1%40epam.com%7C08437a04f690436abce108dde323160d%7Cb41b72d04e9f4c268a69f949f367c91d%7C1%7C0%7C638916462021941023%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=MV6luTeth3rosis1dC2kvVvGBEVSkOzyQGe9HDWftaM%3D&reserved=0
>> ---
>
> https://eur01.safelinks.protection.outlook.com/?
> url=https%3A%2F%2Fgitlab.com%2Fxen-
> project%2Fpeople%2Fdimaprkp4k%2Fxen%2F-
> %2Fjobs%2F11119212994&data=05%7C02%7Cdmytro_prokopchuk1%40epam.com%7C08437a04f690436abce108dde323160d%7Cb41b72d04e9f4c268a69f949f367c91d%7C1%7C0%7C638916462021972965%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=J1GNdrIG1ApqIOqsSyygSZbU%2B3H%2BFvHZKxtBMgz2CXY%3D&reserved=0
>
> Build failure here
Restarted the failed job. Finished successfully.
Dmytro.
>
>> automation/eclair_analysis/ECLAIR/deviations.ecl | 11 +++++++++++
>> docs/misra/deviations.rst | 13 +++++++++++++
>> 2 files changed, 24 insertions(+)
>>
>> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/
>> automation/eclair_analysis/ECLAIR/deviations.ecl
>> index 7f3fd35a33..336aec58c2 100644
>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>> @@ -41,6 +41,17 @@ 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="The 'BUG()' macro is intentionally used in the
>> 'prepare_acpi()' function in specific build configuration
>> +(when the config CONFIG_ACPI is not defined) to trigger an 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)))"}
>> +-doc_end
>> +
>> +-doc_begin="The 'BUG()' macro is intentionally used in
>> 'gicv3_do_LPI'() and 'gicv3_its_setup_collection()' functions
>> +in specific build configuration (when the config CONFIG_HAS_ITS is
>> not defined) 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)))"}
>> +-doc_end
>> +
>> -doc_begin="Proving compliance with respect to Rule 2.2 is generally
>> impossible:
>> see https://eur01.safelinks.protection.outlook.com/?
>> url=https%3A%2F%2Farxiv.org%2Fabs%2F2212.13933&data=05%7C02%7Cdmytro_prokopchuk1%40epam.com%7C08437a04f690436abce108dde323160d%7Cb41b72d04e9f4c268a69f949f367c91d%7C1%7C0%7C638916462021989821%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=N2i2wigU3ol8M2DsYhb8DcwrIvyYEhlbQrlaMlYoWJw%3D&reserved=0 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 2119066531..96eb202502 100644
>> --- a/docs/misra/deviations.rst
>> +++ b/docs/misra/deviations.rst
>> @@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
>> Xen expects developers to ensure code remains safe and
>> reliable in builds,
>> even when debug-only assertions like `ASSERT_UNREACHABLE() are
>> removed.
>>
>> + * - R2.1
>> + - The 'BUG()' macro is intentionally used in the
>> 'prepare_acpi()' function
>> + in specific build configuration (when the config CONFIG_ACPI
>> is not
>> + defined) to trigger an error if ACPI-related features are used
>> incorrectly.
>> + - Tagged as `deliberate` for ECLAIR.
>> +
>> + * - R2.1
>> + - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
>> + 'gicv3_its_setup_collection()' functions in specific build
>> configuration
>> + (when the config CONFIG_HAS_ITS is not defined) 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://eur01.safelinks.protection.outlook.com/?
>> url=https%3A%2F%2Farxiv.org%2Fabs%2F2212.13933&data=05%7C02%7Cdmytro_prokopchuk1%40epam.com%7C08437a04f690436abce108dde323160d%7Cb41b72d04e9f4c268a69f949f367c91d%7C1%7C0%7C638916462022006666%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=fT1IM0bnst9%2FkJ2rI7GiMRkbWJVG%2F%2FD%2B82z3QDVyD9s%3D&reserved=0>`_ for details. Moreover, peer
>
© 2016 - 2025 Red Hat, Inc.