[PATCH] misra: add deviation for PrintErrMesg() function

Dmytro Prokopchuk1 posted 1 patch 2 months, 1 week ago
Patches applied successfully (tree, apply log)
git fetch https://gitlab.com/xen-project/patchew/xen tags/patchew/5944d87aae330246b7dab6eebd04d5d71a7d7e8f.1755608417.git.dmytro._5Fprokopchuk1@epam.com
automation/eclair_analysis/ECLAIR/deviations.ecl | 4 ++++
docs/misra/deviations.rst                        | 7 +++++++
2 files changed, 11 insertions(+)
[PATCH] misra: add deviation for PrintErrMesg() function
Posted by Dmytro Prokopchuk1 2 months, 1 week ago
MISRA C Rule 2.1 states: "A project shall not contain unreachable code."

The function 'PrintErrMesg()' is implemented to never return control to
its caller. At the end of its execution, it calls 'blexit()', which, in
turn, invokes '__builtin_unreachable()'. This makes the 'return false;'
statement in 'read_file()' function unreachable.

Configure Eclair to do not report this violation.

Signed-off-by: Dmytro Prokopchuk <dmytro_prokopchuk1@epam.com>
---
Test CI pipeline:
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/1991518214
---
 automation/eclair_analysis/ECLAIR/deviations.ecl | 4 ++++
 docs/misra/deviations.rst                        | 7 +++++++
 2 files changed, 11 insertions(+)

diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 7f3fd35a33..5c262aa5ad 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -41,6 +41,10 @@ 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="Unreachability caused by the call to the 'PrintErrMesg()' function is deliberate, as it terminates execution, ensuring no control flow continues past this point."
+-config=MC3A2.R2.1,reports+={deliberate, "any_area(^.*PrintErrMesg.*$ && any_loc(file(^xen/common/efi/boot\\.c$)))"}
+-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..8df3c207ff 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -97,6 +97,13 @@ 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
+     - Function `PrintErrMesg()` terminates execution (at the end it calls
+       `blexit()`, which, in turn, invokes `__builtin_unreachable()`), ensuring
+       no code beyond this point is ever reached. This guarantees that execution
+       won't incorrectly proceed or introduce unwanted behavior.
+     - 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
Re: [PATCH] misra: add deviation for PrintErrMesg() function
Posted by Jan Beulich 2 months, 1 week ago
On 19.08.2025 15:12, Dmytro Prokopchuk1 wrote:
> MISRA C Rule 2.1 states: "A project shall not contain unreachable code."
> 
> The function 'PrintErrMesg()' is implemented to never return control to
> its caller. At the end of its execution, it calls 'blexit()', which, in
> turn, invokes '__builtin_unreachable()'. This makes the 'return false;'
> statement in 'read_file()' function unreachable.

I'm disappointed. In earlier review comments I pointed out that there are
two. Yet you say "the", without further disambiguation.

> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -41,6 +41,10 @@ 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="Unreachability caused by the call to the 'PrintErrMesg()' function is deliberate, as it terminates execution, ensuring no control flow continues past this point."
> +-config=MC3A2.R2.1,reports+={deliberate, "any_area(^.*PrintErrMesg.*$ && any_loc(file(^xen/common/efi/boot\\.c$)))"}
> +-doc_end

I don't understand the description here, nor ...

> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -97,6 +97,13 @@ 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
> +     - Function `PrintErrMesg()` terminates execution (at the end it calls
> +       `blexit()`, which, in turn, invokes `__builtin_unreachable()`), ensuring
> +       no code beyond this point is ever reached. This guarantees that execution
> +       won't incorrectly proceed or introduce unwanted behavior.
> +     - Tagged as `deliberate` for ECLAIR.

.. the text here. PrintErrMesg() is noreturn. Why would anything need saying about
it? Isn't the problem here solely with the tail of read_file(), while other uses
of PrintErrMesg() are okay?

Jan
Re: [PATCH] misra: add deviation for PrintErrMesg() function
Posted by Dmytro Prokopchuk1 2 months, 1 week ago

On 8/19/25 16:25, Jan Beulich wrote:
> On 19.08.2025 15:12, Dmytro Prokopchuk1 wrote:
>> MISRA C Rule 2.1 states: "A project shall not contain unreachable code."
>>
>> The function 'PrintErrMesg()' is implemented to never return control to
>> its caller. At the end of its execution, it calls 'blexit()', which, in
>> turn, invokes '__builtin_unreachable()'. This makes the 'return false;'
>> statement in 'read_file()' function unreachable.
> 
> I'm disappointed. In earlier review comments I pointed out that there are
> two. Yet you say "the", without further disambiguation.
> 
>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>> @@ -41,6 +41,10 @@ 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="Unreachability caused by the call to the 'PrintErrMesg()' function is deliberate, as it terminates execution, ensuring no control flow continues past this point."
>> +-config=MC3A2.R2.1,reports+={deliberate, "any_area(^.*PrintErrMesg.*$ && any_loc(file(^xen/common/efi/boot\\.c$)))"}
>> +-doc_end
> 
> I don't understand the description here, nor ...
> 
>> --- a/docs/misra/deviations.rst
>> +++ b/docs/misra/deviations.rst
>> @@ -97,6 +97,13 @@ 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
>> +     - Function `PrintErrMesg()` terminates execution (at the end it calls
>> +       `blexit()`, which, in turn, invokes `__builtin_unreachable()`), ensuring
>> +       no code beyond this point is ever reached. This guarantees that execution
>> +       won't incorrectly proceed or introduce unwanted behavior.
>> +     - Tagged as `deliberate` for ECLAIR.
> 
> .. the text here. PrintErrMesg() is noreturn. Why would anything need saying about
> it? Isn't the problem here solely with the tail of read_file(), while other uses
> of PrintErrMesg() are okay?
> 
> Jan

I'm a little bit confused.

As I understood you proposed to insert the SAF comment before the 
'return' statement (with proper justification).

And current Eclair configuration & descriptions are not good at all.

Am I right?

Dmytro.
Re: [PATCH] misra: add deviation for PrintErrMesg() function
Posted by Jan Beulich 2 months, 1 week ago
On 19.08.2025 16:32, Dmytro Prokopchuk1 wrote:
> On 8/19/25 16:25, Jan Beulich wrote:
>> On 19.08.2025 15:12, Dmytro Prokopchuk1 wrote:
>>> MISRA C Rule 2.1 states: "A project shall not contain unreachable code."
>>>
>>> The function 'PrintErrMesg()' is implemented to never return control to
>>> its caller. At the end of its execution, it calls 'blexit()', which, in
>>> turn, invokes '__builtin_unreachable()'. This makes the 'return false;'
>>> statement in 'read_file()' function unreachable.
>>
>> I'm disappointed. In earlier review comments I pointed out that there are
>> two. Yet you say "the", without further disambiguation.
>>
>>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>>> @@ -41,6 +41,10 @@ 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="Unreachability caused by the call to the 'PrintErrMesg()' function is deliberate, as it terminates execution, ensuring no control flow continues past this point."
>>> +-config=MC3A2.R2.1,reports+={deliberate, "any_area(^.*PrintErrMesg.*$ && any_loc(file(^xen/common/efi/boot\\.c$)))"}
>>> +-doc_end
>>
>> I don't understand the description here, nor ...
>>
>>> --- a/docs/misra/deviations.rst
>>> +++ b/docs/misra/deviations.rst
>>> @@ -97,6 +97,13 @@ 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
>>> +     - Function `PrintErrMesg()` terminates execution (at the end it calls
>>> +       `blexit()`, which, in turn, invokes `__builtin_unreachable()`), ensuring
>>> +       no code beyond this point is ever reached. This guarantees that execution
>>> +       won't incorrectly proceed or introduce unwanted behavior.
>>> +     - Tagged as `deliberate` for ECLAIR.
>>
>> .. the text here. PrintErrMesg() is noreturn. Why would anything need saying about
>> it? Isn't the problem here solely with the tail of read_file(), while other uses
>> of PrintErrMesg() are okay?
> 
> I'm a little bit confused.
> 
> As I understood you proposed to insert the SAF comment before the 
> 'return' statement (with proper justification).
> 
> And current Eclair configuration & descriptions are not good at all.

Not sure how that's related, but apart from this, ...

> Am I right?

... yes. Yet how is what you submitted here related to the issue in read_file(),
which may be addressable by a simple SAF comment (as you say in your reply)?

Jan
Re: [PATCH] misra: add deviation for PrintErrMesg() function
Posted by Dmytro Prokopchuk1 2 months, 1 week ago

On 8/19/25 18:42, Jan Beulich wrote:
> On 19.08.2025 16:32, Dmytro Prokopchuk1 wrote:
>> On 8/19/25 16:25, Jan Beulich wrote:
>>> On 19.08.2025 15:12, Dmytro Prokopchuk1 wrote:
>>>> MISRA C Rule 2.1 states: "A project shall not contain unreachable code."
>>>>
>>>> The function 'PrintErrMesg()' is implemented to never return control to
>>>> its caller. At the end of its execution, it calls 'blexit()', which, in
>>>> turn, invokes '__builtin_unreachable()'. This makes the 'return false;'
>>>> statement in 'read_file()' function unreachable.
>>>
>>> I'm disappointed. In earlier review comments I pointed out that there are
>>> two. Yet you say "the", without further disambiguation.
>>>
>>>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>>>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>>>> @@ -41,6 +41,10 @@ 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="Unreachability caused by the call to the 'PrintErrMesg()' function is deliberate, as it terminates execution, ensuring no control flow continues past this point."
>>>> +-config=MC3A2.R2.1,reports+={deliberate, "any_area(^.*PrintErrMesg.*$ && any_loc(file(^xen/common/efi/boot\\.c$)))"}
>>>> +-doc_end
>>>
>>> I don't understand the description here, nor ...
>>>
>>>> --- a/docs/misra/deviations.rst
>>>> +++ b/docs/misra/deviations.rst
>>>> @@ -97,6 +97,13 @@ 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
>>>> +     - Function `PrintErrMesg()` terminates execution (at the end it calls
>>>> +       `blexit()`, which, in turn, invokes `__builtin_unreachable()`), ensuring
>>>> +       no code beyond this point is ever reached. This guarantees that execution
>>>> +       won't incorrectly proceed or introduce unwanted behavior.
>>>> +     - Tagged as `deliberate` for ECLAIR.
>>>
>>> .. the text here. PrintErrMesg() is noreturn. Why would anything need saying about
>>> it? Isn't the problem here solely with the tail of read_file(), while other uses
>>> of PrintErrMesg() are okay?
>>
>> I'm a little bit confused.
>>
>> As I understood you proposed to insert the SAF comment before the
>> 'return' statement (with proper justification).
>>
>> And current Eclair configuration & descriptions are not good at all.
> 
> Not sure how that's related, but apart from this, ...
> 
>> Am I right?
> 
> ... yes. Yet how is what you submitted here related to the issue in read_file(),
> which may be addressable by a simple SAF comment (as you say in your reply)?
> 
> Jan

The Eclair reports violation as follows:
"call to function `PrintErrMesg(const CHAR16*, EFI_STATUS)' (unit 
`xen/common/efi/boot.c' with target `xen/arch/arm/efi/boot.o') is one 
cause of unreachability of the next statement"

So, patch was about to ignore violations in file 'xen/common/efi/boot.c'
(actually function read_file() is there) where appears text 'PrintErrMesg'.

Probably this is too unclear. And violation location (read_file()) 
should be explicitly specified...

 From other side simple SAF-xx-safe could address this case as well.

Dmytro.