docs/misra/rules.rst | 13 ++++++++++++- docs/misra/safe.json | 8 ++++++++ xen/arch/arm/psci.c | 1 + xen/arch/x86/shutdown.c | 1 + xen/include/xen/bug.h | 2 ++ 5 files changed, 24 insertions(+), 1 deletion(-)
From: Stefano Stabellini <stefano.stabellini@amd.com>
During the discussions that led to the acceptance of Rule 2.1, we
decided on a few exceptions that were not properly recorded in
rules.rst. Add them now.
Signed-off-by: Stefano Stabellini <stefano.stabellini@amd.com>
Acked-by: Jan Beulich <jbeulich@suse.com>
---
Nicola, does this work with ECLAIR?
I am referring to the locations of the SAF-2-safe tag on top of
call_psci_system_off, BUG, etc.
Changes in v3:
- added SAF-2-safe to safe.json
- added a few SAF-2-safe examples
---
docs/misra/rules.rst | 13 ++++++++++++-
docs/misra/safe.json | 8 ++++++++
xen/arch/arm/psci.c | 1 +
xen/arch/x86/shutdown.c | 1 +
xen/include/xen/bug.h | 2 ++
5 files changed, 24 insertions(+), 1 deletion(-)
diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
index 34916e266a..82de4c645d 100644
--- a/docs/misra/rules.rst
+++ b/docs/misra/rules.rst
@@ -107,7 +107,18 @@ maintainers if you want to suggest a change.
* - `Rule 2.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_01_1.c>`_
- Required
- A project shall not contain unreachable code
- -
+ - The following are allowed:
+ - Invariantly constant conditions, e.g. if(IS_ENABLED(CONFIG_HVM)) { S; }
+ - Switch with a controlling value statically determined not to
+ match one or more case statements
+ - Functions that are intended to be referenced only from
+ assembly code (e.g. 'do_trap_fiq')
+ - Deliberate unreachability caused by certain macros/functions,
+ e.g. BUG, assert_failed, panic, etc. See safe.json.
+ - asm-offsets.c, as they are not linked deliberately, because
+ they are used to generate definitions for asm modules
+ - Declarations without initializer are safe, as they are not
+ executed
* - `Rule 2.6 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_06.c>`_
- Advisory
diff --git a/docs/misra/safe.json b/docs/misra/safe.json
index 39c5c056c7..fc96a99fd5 100644
--- a/docs/misra/safe.json
+++ b/docs/misra/safe.json
@@ -20,6 +20,14 @@
},
{
"id": "SAF-2-safe",
+ "analyser": {
+ "eclair": "MC3R1.R2.1"
+ },
+ "name": "Rule 2.1: deliberate unreachability",
+ "text": "Macro or function designed to be unreachable."
+ },
+ {
+ "id": "SAF-3-safe",
"analyser": {},
"name": "Sentinel",
"text": "Next ID to be used"
diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
index 695d2fa1f1..2a8527cacc 100644
--- a/xen/arch/arm/psci.c
+++ b/xen/arch/arm/psci.c
@@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
}
}
+/* SAF-2-safe */
void call_psci_system_off(void)
{
if ( psci_ver > PSCI_VERSION(0, 1) )
diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
index 7619544d14..47e0f59024 100644
--- a/xen/arch/x86/shutdown.c
+++ b/xen/arch/x86/shutdown.c
@@ -118,6 +118,7 @@ static inline void kb_wait(void)
break;
}
+/* SAF-2-safe */
static void noreturn cf_check __machine_halt(void *unused)
{
local_irq_disable();
diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
index e8a4eea71a..d47c54f034 100644
--- a/xen/include/xen/bug.h
+++ b/xen/include/xen/bug.h
@@ -117,6 +117,7 @@ struct bug_frame {
#endif
#ifndef BUG
+/* SAF-2-safe */
#define BUG() do { \
BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
unreachable(); \
@@ -124,6 +125,7 @@ struct bug_frame {
#endif
#ifndef assert_failed
+/* SAF-2-safe */
#define assert_failed(msg) do { \
BUG_FRAME(BUGFRAME_assert, __LINE__, __FILE__, 1, msg); \
unreachable(); \
--
2.25.1Hi Stefano,
On 09/09/2023 00:03, Stefano Stabellini wrote:
> From: Stefano Stabellini <stefano.stabellini@amd.com>
>
> During the discussions that led to the acceptance of Rule 2.1, we
> decided on a few exceptions that were not properly recorded in
> rules.rst. Add them now.
>
> Signed-off-by: Stefano Stabellini <stefano.stabellini@amd.com>
> Acked-by: Jan Beulich <jbeulich@suse.com>
> ---
> Nicola, does this work with ECLAIR?
>
> I am referring to the locations of the SAF-2-safe tag on top of
> call_psci_system_off, BUG, etc.
>
> Changes in v3:
> - added SAF-2-safe to safe.json
> - added a few SAF-2-safe examples
> ---
> docs/misra/rules.rst | 13 ++++++++++++-
> docs/misra/safe.json | 8 ++++++++
> xen/arch/arm/psci.c | 1 +
> xen/arch/x86/shutdown.c | 1 +
> xen/include/xen/bug.h | 2 ++
> 5 files changed, 24 insertions(+), 1 deletion(-)
>
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index 34916e266a..82de4c645d 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -107,7 +107,18 @@ maintainers if you want to suggest a change.
> * - `Rule 2.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_01_1.c>`_
> - Required
> - A project shall not contain unreachable code
> - -
> + - The following are allowed:
> + - Invariantly constant conditions, e.g. if(IS_ENABLED(CONFIG_HVM)) { S; }
> + - Switch with a controlling value statically determined not to
> + match one or more case statements
> + - Functions that are intended to be referenced only from
> + assembly code (e.g. 'do_trap_fiq')
> + - Deliberate unreachability caused by certain macros/functions,
> + e.g. BUG, assert_failed, panic, etc. See safe.json.
> + - asm-offsets.c, as they are not linked deliberately, because
> + they are used to generate definitions for asm modules
> + - Declarations without initializer are safe, as they are not
> + executed
>
> * - `Rule 2.6 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_06.c>`_
> - Advisory
> diff --git a/docs/misra/safe.json b/docs/misra/safe.json
> index 39c5c056c7..fc96a99fd5 100644
> --- a/docs/misra/safe.json
> +++ b/docs/misra/safe.json
> @@ -20,6 +20,14 @@
> },
> {
> "id": "SAF-2-safe",
> + "analyser": {
> + "eclair": "MC3R1.R2.1"
> + },
> + "name": "Rule 2.1: deliberate unreachability",
> + "text": "Macro or function designed to be unreachable."
> + },
> + {
> + "id": "SAF-3-safe",
> "analyser": {},
> "name": "Sentinel",
> "text": "Next ID to be used"
> diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
> index 695d2fa1f1..2a8527cacc 100644
> --- a/xen/arch/arm/psci.c
> +++ b/xen/arch/arm/psci.c
> @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
> }
> }
>
> +/* SAF-2-safe */
I think any use of SAF-2-safe should be accompanied with an attribute...
> void call_psci_system_off(void)
... noreturn for function or ...
> {
> if ( psci_ver > PSCI_VERSION(0, 1) )
> diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
> index 7619544d14..47e0f59024 100644
> --- a/xen/arch/x86/shutdown.c
> +++ b/xen/arch/x86/shutdown.c
> @@ -118,6 +118,7 @@ static inline void kb_wait(void)
> break;
> }
>
> +/* SAF-2-safe */
> static void noreturn cf_check __machine_halt(void *unused)
> {
> local_irq_disable();
> diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
> index e8a4eea71a..d47c54f034 100644
> --- a/xen/include/xen/bug.h
> +++ b/xen/include/xen/bug.h
> @@ -117,6 +117,7 @@ struct bug_frame {
> #endif
>
> #ifndef BUG
> +/* SAF-2-safe */
> #define BUG() do { \
> BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
> unreachable(); \
... unreachable for macros. But the /* SAF-2-safe */ feels a little bit
redundant when a function is marked as 'noreturn'.
Is there any way to teach eclair about noreturn?
Cheers,
--
Julien Grall
On Mon, 11 Sep 2023, Julien Grall wrote:
> Hi Stefano,
>
> On 09/09/2023 00:03, Stefano Stabellini wrote:
> > From: Stefano Stabellini <stefano.stabellini@amd.com>
> >
> > During the discussions that led to the acceptance of Rule 2.1, we
> > decided on a few exceptions that were not properly recorded in
> > rules.rst. Add them now.
> >
> > Signed-off-by: Stefano Stabellini <stefano.stabellini@amd.com>
> > Acked-by: Jan Beulich <jbeulich@suse.com>
> > ---
> > Nicola, does this work with ECLAIR?
> >
> > I am referring to the locations of the SAF-2-safe tag on top of
> > call_psci_system_off, BUG, etc.
> >
> > Changes in v3:
> > - added SAF-2-safe to safe.json
> > - added a few SAF-2-safe examples
> > ---
> > docs/misra/rules.rst | 13 ++++++++++++-
> > docs/misra/safe.json | 8 ++++++++
> > xen/arch/arm/psci.c | 1 +
> > xen/arch/x86/shutdown.c | 1 +
> > xen/include/xen/bug.h | 2 ++
> > 5 files changed, 24 insertions(+), 1 deletion(-)
> >
> > diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> > index 34916e266a..82de4c645d 100644
> > --- a/docs/misra/rules.rst
> > +++ b/docs/misra/rules.rst
> > @@ -107,7 +107,18 @@ maintainers if you want to suggest a change.
> > * - `Rule 2.1
> > <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_01_1.c>`_
> > - Required
> > - A project shall not contain unreachable code
> > - -
> > + - The following are allowed:
> > + - Invariantly constant conditions, e.g. if(IS_ENABLED(CONFIG_HVM))
> > { S; }
> > + - Switch with a controlling value statically determined not to
> > + match one or more case statements
> > + - Functions that are intended to be referenced only from
> > + assembly code (e.g. 'do_trap_fiq')
> > + - Deliberate unreachability caused by certain macros/functions,
> > + e.g. BUG, assert_failed, panic, etc. See safe.json.
> > + - asm-offsets.c, as they are not linked deliberately, because
> > + they are used to generate definitions for asm modules
> > + - Declarations without initializer are safe, as they are not
> > + executed
> > * - `Rule 2.6
> > <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_06.c>`_
> > - Advisory
> > diff --git a/docs/misra/safe.json b/docs/misra/safe.json
> > index 39c5c056c7..fc96a99fd5 100644
> > --- a/docs/misra/safe.json
> > +++ b/docs/misra/safe.json
> > @@ -20,6 +20,14 @@
> > },
> > {
> > "id": "SAF-2-safe",
> > + "analyser": {
> > + "eclair": "MC3R1.R2.1"
> > + },
> > + "name": "Rule 2.1: deliberate unreachability",
> > + "text": "Macro or function designed to be unreachable."
> > + },
> > + {
> > + "id": "SAF-3-safe",
> > "analyser": {},
> > "name": "Sentinel",
> > "text": "Next ID to be used"
> > diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
> > index 695d2fa1f1..2a8527cacc 100644
> > --- a/xen/arch/arm/psci.c
> > +++ b/xen/arch/arm/psci.c
> > @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
> > }
> > }
> > +/* SAF-2-safe */
>
> I think any use of SAF-2-safe should be accompanied with an attribute...
>
> > void call_psci_system_off(void)
>
> ... noreturn for function or ...
>
> > {
> > if ( psci_ver > PSCI_VERSION(0, 1) )
> > diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
> > index 7619544d14..47e0f59024 100644
> > --- a/xen/arch/x86/shutdown.c
> > +++ b/xen/arch/x86/shutdown.c
> > @@ -118,6 +118,7 @@ static inline void kb_wait(void)
> > break;
> > }
> > +/* SAF-2-safe */
> > static void noreturn cf_check __machine_halt(void *unused)
> > {
> > local_irq_disable();
> > diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
> > index e8a4eea71a..d47c54f034 100644
> > --- a/xen/include/xen/bug.h
> > +++ b/xen/include/xen/bug.h
> > @@ -117,6 +117,7 @@ struct bug_frame {
> > #endif
> > #ifndef BUG
> > +/* SAF-2-safe */
> > #define BUG() do { \
> > BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
> > unreachable(); \
>
> ... unreachable for macros. But the /* SAF-2-safe */ feels a little bit
> redundant when a function is marked as 'noreturn'.
>
> Is there any way to teach eclair about noreturn?
Actually I had the same thought while writing this patch. If we can
adopt unreachable and noreturn consistently maybe we don't need
SAF-2-safe. If the checker can support it.
Nicola, what do you think?
>> > diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
>> > index 695d2fa1f1..2a8527cacc 100644
>> > --- a/xen/arch/arm/psci.c
>> > +++ b/xen/arch/arm/psci.c
>> > @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
>> > }
>> > }
>> > +/* SAF-2-safe */
>>
>> I think any use of SAF-2-safe should be accompanied with an
>> attribute...
>>
>> > void call_psci_system_off(void)
>>
>> ... noreturn for function or ...
>>
>> > {
>> > if ( psci_ver > PSCI_VERSION(0, 1) )
>> > diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
>> > index 7619544d14..47e0f59024 100644
>> > --- a/xen/arch/x86/shutdown.c
>> > +++ b/xen/arch/x86/shutdown.c
>> > @@ -118,6 +118,7 @@ static inline void kb_wait(void)
>> > break;
>> > }
>> > +/* SAF-2-safe */
>> > static void noreturn cf_check __machine_halt(void *unused)
>> > {
>> > local_irq_disable();
>> > diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
>> > index e8a4eea71a..d47c54f034 100644
>> > --- a/xen/include/xen/bug.h
>> > +++ b/xen/include/xen/bug.h
>> > @@ -117,6 +117,7 @@ struct bug_frame {
>> > #endif
>> > #ifndef BUG
>> > +/* SAF-2-safe */
>> > #define BUG() do { \
>> > BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
>> > unreachable(); \
>>
>> ... unreachable for macros. But the /* SAF-2-safe */ feels a little
>> bit
>> redundant when a function is marked as 'noreturn'.
>>
>> Is there any way to teach eclair about noreturn?
>
> Actually I had the same thought while writing this patch. If we can
> adopt unreachable and noreturn consistently maybe we don't need
> SAF-2-safe. If the checker can support it.
>
> Nicola, what do you think?
A couple of remarks:
- if you put the noreturn attribute on some functions, then surely the
code after those is
reported as unreachable. ECLAIR should pick up all forms of noreturn
automatically; otherwise, a simple configuration can be used.
- Note that the cause of unreachability in the vast majority of cases is
the call to
__builtin_unreachable(), therefore a textual deviation on the definition
of unreachable, plus
a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF
comment is not
sufficient, since deviations comments are meant to be applied at the top
expansion location,
which is not on the macro definition).
This is what it should look like, roughly:
-config=MC3R1.R2.1,reports+={deliberate,
"any_area(any_loc(text(^<REGEX>$, -1)))"}
#if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
/* SAF-2-safe */
#define unreachable() do {} while (1)
#else
/* SAF-2-safe */
#define unreachable() __builtin_unreachable()
#endif
where REGEX will match the translation of SAF-2-safe.
However, this will then entail that *some* SAF comments are treated
specially and, moreover,
that some modification to the definition of unreachable won't work
(e.g.
#define M() __builtin_unreachable()
/* SAF-2-safe */
#define unreachable() M()
My opinion is that it's far easier for this to be an eclair
configuration (which has the
advantage not to depend on the exact definition of unreachable) and then
perhaps a comment
above it explaining the situation.
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)
Hi,
> On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote:
>
>>> > diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
>>> > index 695d2fa1f1..2a8527cacc 100644
>>> > --- a/xen/arch/arm/psci.c
>>> > +++ b/xen/arch/arm/psci.c
>>> > @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
>>> > }
>>> > }
>>> > +/* SAF-2-safe */
>>> I think any use of SAF-2-safe should be accompanied with an attribute...
>>> > void call_psci_system_off(void)
>>> ... noreturn for function or ...
>>> > {
>>> > if ( psci_ver > PSCI_VERSION(0, 1) )
>>> > diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
>>> > index 7619544d14..47e0f59024 100644
>>> > --- a/xen/arch/x86/shutdown.c
>>> > +++ b/xen/arch/x86/shutdown.c
>>> > @@ -118,6 +118,7 @@ static inline void kb_wait(void)
>>> > break;
>>> > }
>>> > +/* SAF-2-safe */
>>> > static void noreturn cf_check __machine_halt(void *unused)
>>> > {
>>> > local_irq_disable();
>>> > diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
>>> > index e8a4eea71a..d47c54f034 100644
>>> > --- a/xen/include/xen/bug.h
>>> > +++ b/xen/include/xen/bug.h
>>> > @@ -117,6 +117,7 @@ struct bug_frame {
>>> > #endif
>>> > #ifndef BUG
>>> > +/* SAF-2-safe */
>>> > #define BUG() do { \
>>> > BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
>>> > unreachable(); \
>>> ... unreachable for macros. But the /* SAF-2-safe */ feels a little bit
>>> redundant when a function is marked as 'noreturn'.
>>> Is there any way to teach eclair about noreturn?
>> Actually I had the same thought while writing this patch. If we can
>> adopt unreachable and noreturn consistently maybe we don't need
>> SAF-2-safe. If the checker can support it.
>> Nicola, what do you think?
>
> A couple of remarks:
> - if you put the noreturn attribute on some functions, then surely the code after those is
> reported as unreachable. ECLAIR should pick up all forms of noreturn automatically; otherwise, a simple configuration can be used.
>
> - Note that the cause of unreachability in the vast majority of cases is the call to
> __builtin_unreachable(), therefore a textual deviation on the definition of unreachable, plus
> a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF comment is not
> sufficient, since deviations comments are meant to be applied at the top expansion location,
> which is not on the macro definition).
> This is what it should look like, roughly:
>
> -config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(text(^<REGEX>$, -1)))"}
>
> #if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
> /* SAF-2-safe */
> #define unreachable() do {} while (1)
> #else
> /* SAF-2-safe */
> #define unreachable() __builtin_unreachable()
> #endif
>
> where REGEX will match the translation of SAF-2-safe.
>
> However, this will then entail that *some* SAF comments are treated specially and, moreover,
> that some modification to the definition of unreachable won't work
> (e.g.
> #define M() __builtin_unreachable()
> /* SAF-2-safe */
> #define unreachable() M()
>
> My opinion is that it's far easier for this to be an eclair configuration (which has the
> advantage not to depend on the exact definition of unreachable) and then perhaps a comment
> above it explaining the situation.
I agree here and it is easier to make an overall exception where we list the cases
where this is acceptable (ie all flavors of unreacheable) and document that eclair
was configured using "xxxx" to handle this.
Cheers
Bertrand
>
> --
> Nicola Vetrini, BSc
> Software Engineer, BUGSENG srl (https://bugseng.com)
On Wed, 27 Sep 2023, Bertrand Marquis wrote:
> > On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote:
> >
> >>> > diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
> >>> > index 695d2fa1f1..2a8527cacc 100644
> >>> > --- a/xen/arch/arm/psci.c
> >>> > +++ b/xen/arch/arm/psci.c
> >>> > @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
> >>> > }
> >>> > }
> >>> > +/* SAF-2-safe */
> >>> I think any use of SAF-2-safe should be accompanied with an attribute...
> >>> > void call_psci_system_off(void)
> >>> ... noreturn for function or ...
> >>> > {
> >>> > if ( psci_ver > PSCI_VERSION(0, 1) )
> >>> > diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
> >>> > index 7619544d14..47e0f59024 100644
> >>> > --- a/xen/arch/x86/shutdown.c
> >>> > +++ b/xen/arch/x86/shutdown.c
> >>> > @@ -118,6 +118,7 @@ static inline void kb_wait(void)
> >>> > break;
> >>> > }
> >>> > +/* SAF-2-safe */
> >>> > static void noreturn cf_check __machine_halt(void *unused)
> >>> > {
> >>> > local_irq_disable();
> >>> > diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
> >>> > index e8a4eea71a..d47c54f034 100644
> >>> > --- a/xen/include/xen/bug.h
> >>> > +++ b/xen/include/xen/bug.h
> >>> > @@ -117,6 +117,7 @@ struct bug_frame {
> >>> > #endif
> >>> > #ifndef BUG
> >>> > +/* SAF-2-safe */
> >>> > #define BUG() do { \
> >>> > BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
> >>> > unreachable(); \
> >>> ... unreachable for macros. But the /* SAF-2-safe */ feels a little bit
> >>> redundant when a function is marked as 'noreturn'.
> >>> Is there any way to teach eclair about noreturn?
> >> Actually I had the same thought while writing this patch. If we can
> >> adopt unreachable and noreturn consistently maybe we don't need
> >> SAF-2-safe. If the checker can support it.
> >> Nicola, what do you think?
> >
> > A couple of remarks:
> > - if you put the noreturn attribute on some functions, then surely the code after those is
> > reported as unreachable. ECLAIR should pick up all forms of noreturn automatically; otherwise, a simple configuration can be used.
> >
> > - Note that the cause of unreachability in the vast majority of cases is the call to
> > __builtin_unreachable(), therefore a textual deviation on the definition of unreachable, plus
> > a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF comment is not
> > sufficient, since deviations comments are meant to be applied at the top expansion location,
> > which is not on the macro definition).
> > This is what it should look like, roughly:
> >
> > -config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(text(^<REGEX>$, -1)))"}
> >
> > #if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
> > /* SAF-2-safe */
> > #define unreachable() do {} while (1)
> > #else
> > /* SAF-2-safe */
> > #define unreachable() __builtin_unreachable()
> > #endif
> >
> > where REGEX will match the translation of SAF-2-safe.
> >
> > However, this will then entail that *some* SAF comments are treated specially and, moreover,
> > that some modification to the definition of unreachable won't work
> > (e.g.
> > #define M() __builtin_unreachable()
> > /* SAF-2-safe */
> > #define unreachable() M()
> >
> > My opinion is that it's far easier for this to be an eclair configuration (which has the
> > advantage not to depend on the exact definition of unreachable) and then perhaps a comment
> > above it explaining the situation.
>
> I agree here and it is easier to make an overall exception where we list the cases
> where this is acceptable (ie all flavors of unreacheable) and document that eclair
> was configured using "xxxx" to handle this.
In that case it looks like we all agree that we can go ahead with this
patch with just the changes to docs/misra/rules.rst to add rule 2.1 and
remove everything else. Which is v2 of this patch:
https://marc.info/?l=xen-devel&m=169283027729298
Henry, can I get one more release-ack for v2 of this patch (only changes
to docs/misra, no code changes)?
Also Bertrand can you provide a formal Ack for v2?
I do think we should have a document to track this kind of deviations
that are not managed by safe.json or exclude-list.json. But I think for
now the rules.rst notes and the ECLAIR config file (which is under
xen.git) will suffice.
Hi Stefano,
> On Sep 28, 2023, at 08:40, Stefano Stabellini <sstabellini@kernel.org> wrote:
>
> On Wed, 27 Sep 2023, Bertrand Marquis wrote:
>>> On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote:
>>>
>>>>>> diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
>>>>>> index 695d2fa1f1..2a8527cacc 100644
>>>>>> --- a/xen/arch/arm/psci.c
>>>>>> +++ b/xen/arch/arm/psci.c
>>>>>> @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
>>>>>> }
>>>>>> }
>>>>>> +/* SAF-2-safe */
>>>>> I think any use of SAF-2-safe should be accompanied with an attribute...
>>>>>> void call_psci_system_off(void)
>>>>> ... noreturn for function or ...
>>>>>> {
>>>>>> if ( psci_ver > PSCI_VERSION(0, 1) )
>>>>>> diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
>>>>>> index 7619544d14..47e0f59024 100644
>>>>>> --- a/xen/arch/x86/shutdown.c
>>>>>> +++ b/xen/arch/x86/shutdown.c
>>>>>> @@ -118,6 +118,7 @@ static inline void kb_wait(void)
>>>>>> break;
>>>>>> }
>>>>>> +/* SAF-2-safe */
>>>>>> static void noreturn cf_check __machine_halt(void *unused)
>>>>>> {
>>>>>> local_irq_disable();
>>>>>> diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
>>>>>> index e8a4eea71a..d47c54f034 100644
>>>>>> --- a/xen/include/xen/bug.h
>>>>>> +++ b/xen/include/xen/bug.h
>>>>>> @@ -117,6 +117,7 @@ struct bug_frame {
>>>>>> #endif
>>>>>> #ifndef BUG
>>>>>> +/* SAF-2-safe */
>>>>>> #define BUG() do { \
>>>>>> BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
>>>>>> unreachable(); \
>>>>> ... unreachable for macros. But the /* SAF-2-safe */ feels a little bit
>>>>> redundant when a function is marked as 'noreturn'.
>>>>> Is there any way to teach eclair about noreturn?
>>>> Actually I had the same thought while writing this patch. If we can
>>>> adopt unreachable and noreturn consistently maybe we don't need
>>>> SAF-2-safe. If the checker can support it.
>>>> Nicola, what do you think?
>>>
>>> A couple of remarks:
>>> - if you put the noreturn attribute on some functions, then surely the code after those is
>>> reported as unreachable. ECLAIR should pick up all forms of noreturn automatically; otherwise, a simple configuration can be used.
>>>
>>> - Note that the cause of unreachability in the vast majority of cases is the call to
>>> __builtin_unreachable(), therefore a textual deviation on the definition of unreachable, plus
>>> a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF comment is not
>>> sufficient, since deviations comments are meant to be applied at the top expansion location,
>>> which is not on the macro definition).
>>> This is what it should look like, roughly:
>>>
>>> -config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(text(^<REGEX>$, -1)))"}
>>>
>>> #if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
>>> /* SAF-2-safe */
>>> #define unreachable() do {} while (1)
>>> #else
>>> /* SAF-2-safe */
>>> #define unreachable() __builtin_unreachable()
>>> #endif
>>>
>>> where REGEX will match the translation of SAF-2-safe.
>>>
>>> However, this will then entail that *some* SAF comments are treated specially and, moreover,
>>> that some modification to the definition of unreachable won't work
>>> (e.g.
>>> #define M() __builtin_unreachable()
>>> /* SAF-2-safe */
>>> #define unreachable() M()
>>>
>>> My opinion is that it's far easier for this to be an eclair configuration (which has the
>>> advantage not to depend on the exact definition of unreachable) and then perhaps a comment
>>> above it explaining the situation.
>>
>> I agree here and it is easier to make an overall exception where we list the cases
>> where this is acceptable (ie all flavors of unreacheable) and document that eclair
>> was configured using "xxxx" to handle this.
>
> In that case it looks like we all agree that we can go ahead with this
> patch with just the changes to docs/misra/rules.rst to add rule 2.1 and
> remove everything else. Which is v2 of this patch:
> https://marc.info/?l=xen-devel&m=169283027729298
>
> Henry, can I get one more release-ack for v2 of this patch (only changes
> to docs/misra, no code changes)?
Sorry for the late reply, I was waiting for the RC1 to come out first. I checked that patch and I
think you can add my release-ack with Bertrand’s comments fixed.
Kind regards,
Henry
>
> Also Bertrand can you provide a formal Ack for v2?
>
> On 28 Sep 2023, at 02:40, Stefano Stabellini <sstabellini@kernel.org> wrote:
>
> On Wed, 27 Sep 2023, Bertrand Marquis wrote:
>>> On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote:
>>>
>>>>>> diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
>>>>>> index 695d2fa1f1..2a8527cacc 100644
>>>>>> --- a/xen/arch/arm/psci.c
>>>>>> +++ b/xen/arch/arm/psci.c
>>>>>> @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
>>>>>> }
>>>>>> }
>>>>>> +/* SAF-2-safe */
>>>>> I think any use of SAF-2-safe should be accompanied with an attribute...
>>>>>> void call_psci_system_off(void)
>>>>> ... noreturn for function or ...
>>>>>> {
>>>>>> if ( psci_ver > PSCI_VERSION(0, 1) )
>>>>>> diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
>>>>>> index 7619544d14..47e0f59024 100644
>>>>>> --- a/xen/arch/x86/shutdown.c
>>>>>> +++ b/xen/arch/x86/shutdown.c
>>>>>> @@ -118,6 +118,7 @@ static inline void kb_wait(void)
>>>>>> break;
>>>>>> }
>>>>>> +/* SAF-2-safe */
>>>>>> static void noreturn cf_check __machine_halt(void *unused)
>>>>>> {
>>>>>> local_irq_disable();
>>>>>> diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
>>>>>> index e8a4eea71a..d47c54f034 100644
>>>>>> --- a/xen/include/xen/bug.h
>>>>>> +++ b/xen/include/xen/bug.h
>>>>>> @@ -117,6 +117,7 @@ struct bug_frame {
>>>>>> #endif
>>>>>> #ifndef BUG
>>>>>> +/* SAF-2-safe */
>>>>>> #define BUG() do { \
>>>>>> BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
>>>>>> unreachable(); \
>>>>> ... unreachable for macros. But the /* SAF-2-safe */ feels a little bit
>>>>> redundant when a function is marked as 'noreturn'.
>>>>> Is there any way to teach eclair about noreturn?
>>>> Actually I had the same thought while writing this patch. If we can
>>>> adopt unreachable and noreturn consistently maybe we don't need
>>>> SAF-2-safe. If the checker can support it.
>>>> Nicola, what do you think?
>>>
>>> A couple of remarks:
>>> - if you put the noreturn attribute on some functions, then surely the code after those is
>>> reported as unreachable. ECLAIR should pick up all forms of noreturn automatically; otherwise, a simple configuration can be used.
>>>
>>> - Note that the cause of unreachability in the vast majority of cases is the call to
>>> __builtin_unreachable(), therefore a textual deviation on the definition of unreachable, plus
>>> a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF comment is not
>>> sufficient, since deviations comments are meant to be applied at the top expansion location,
>>> which is not on the macro definition).
>>> This is what it should look like, roughly:
>>>
>>> -config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(text(^<REGEX>$, -1)))"}
>>>
>>> #if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
>>> /* SAF-2-safe */
>>> #define unreachable() do {} while (1)
>>> #else
>>> /* SAF-2-safe */
>>> #define unreachable() __builtin_unreachable()
>>> #endif
>>>
>>> where REGEX will match the translation of SAF-2-safe.
>>>
>>> However, this will then entail that *some* SAF comments are treated specially and, moreover,
>>> that some modification to the definition of unreachable won't work
>>> (e.g.
>>> #define M() __builtin_unreachable()
>>> /* SAF-2-safe */
>>> #define unreachable() M()
>>>
>>> My opinion is that it's far easier for this to be an eclair configuration (which has the
>>> advantage not to depend on the exact definition of unreachable) and then perhaps a comment
>>> above it explaining the situation.
>>
>> I agree here and it is easier to make an overall exception where we list the cases
>> where this is acceptable (ie all flavors of unreacheable) and document that eclair
>> was configured using "xxxx" to handle this.
>
> In that case it looks like we all agree that we can go ahead with this
> patch with just the changes to docs/misra/rules.rst to add rule 2.1 and
> remove everything else. Which is v2 of this patch:
> https://marc.info/?l=xen-devel&m=169283027729298
>
> Henry, can I get one more release-ack for v2 of this patch (only changes
> to docs/misra, no code changes)?
>
> Also Bertrand can you provide a formal Ack for v2?
>
Done, you just need to handle the comment from Julien for it.
Cheers
Bertrand
>
> I do think we should have a document to track this kind of deviations
> that are not managed by safe.json or exclude-list.json. But I think for
> now the rules.rst notes and the ECLAIR config file (which is under
> xen.git) will suffice.
On 27.09.2023 10:14, Bertrand Marquis wrote: >> On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote: >> My opinion is that it's far easier for this to be an eclair configuration (which has the >> advantage not to depend on the exact definition of unreachable) and then perhaps a comment >> above it explaining the situation. > > I agree here and it is easier to make an overall exception where we list the cases > where this is acceptable (ie all flavors of unreacheable) and document that eclair > was configured using "xxxx" to handle this. What about cppcheck then, for example? Jan
Hi Jan, > On 27 Sep 2023, at 10:23, Jan Beulich <jbeulich@suse.com> wrote: > > On 27.09.2023 10:14, Bertrand Marquis wrote: >>> On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote: >>> My opinion is that it's far easier for this to be an eclair configuration (which has the >>> advantage not to depend on the exact definition of unreachable) and then perhaps a comment >>> above it explaining the situation. >> >> I agree here and it is easier to make an overall exception where we list the cases >> where this is acceptable (ie all flavors of unreacheable) and document that eclair >> was configured using "xxxx" to handle this. > > What about cppcheck then, for example? Good point we should check if cppcheck or coverity can do such things. @Luca: any idea ? Cheers Bertrand > > Jan >
> On 27 Sep 2023, at 09:35, Bertrand Marquis <Bertrand.Marquis@arm.com> wrote: > > Hi Jan, > >> On 27 Sep 2023, at 10:23, Jan Beulich <jbeulich@suse.com> wrote: >> >> On 27.09.2023 10:14, Bertrand Marquis wrote: >>>> On 27 Sep 2023, at 09:53, Nicola Vetrini <nicola.vetrini@bugseng.com> wrote: >>>> My opinion is that it's far easier for this to be an eclair configuration (which has the >>>> advantage not to depend on the exact definition of unreachable) and then perhaps a comment >>>> above it explaining the situation. >>> >>> I agree here and it is easier to make an overall exception where we list the cases >>> where this is acceptable (ie all flavors of unreacheable) and document that eclair >>> was configured using "xxxx" to handle this. >> >> What about cppcheck then, for example? > > Good point we should check if cppcheck or coverity can do such things. > @Luca: any idea ? So, for cppcheck I don’t think we have such granularity, the only thing we can do are suppress all violations for a file, suppress some violations for a file or suppress globally all violations regarding certain rules. For coverity, I’ve found the way to remove files (translation units) from the report, but I didn’t find anything about how to specify some patterns to be excluded. For now I can only exclude entire files or I can exclude rules globally. I will try to get some support from Synopsys to see if there is any way to specify some exclusion pattern for specific rules. Anyway I’ve run Coverity and for the 2.1 it is finding 14 violations but none of them are about __builtin_unreachable(). I’ve also run Cppcheck and it is not complaining, not that I was looking for it to be a benchmark in any case! So I guess Eclair is more strict on the checks and needs to have a proper configuration that can’t be generalised for all the tools. Cheers, Luca
On 09.09.2023 01:03, Stefano Stabellini wrote:
> From: Stefano Stabellini <stefano.stabellini@amd.com>
>
> During the discussions that led to the acceptance of Rule 2.1, we
> decided on a few exceptions that were not properly recorded in
> rules.rst. Add them now.
>
> Signed-off-by: Stefano Stabellini <stefano.stabellini@amd.com>
> Acked-by: Jan Beulich <jbeulich@suse.com>
> ---
> Nicola, does this work with ECLAIR?
>
> I am referring to the locations of the SAF-2-safe tag on top of
> call_psci_system_off, BUG, etc.
>
> Changes in v3:
> - added SAF-2-safe to safe.json
> - added a few SAF-2-safe examples
> ---
> docs/misra/rules.rst | 13 ++++++++++++-
> docs/misra/safe.json | 8 ++++++++
> xen/arch/arm/psci.c | 1 +
> xen/arch/x86/shutdown.c | 1 +
> xen/include/xen/bug.h | 2 ++
> 5 files changed, 24 insertions(+), 1 deletion(-)
>
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index 34916e266a..82de4c645d 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -107,7 +107,18 @@ maintainers if you want to suggest a change.
> * - `Rule 2.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_01_1.c>`_
> - Required
> - A project shall not contain unreachable code
> - -
> + - The following are allowed:
> + - Invariantly constant conditions, e.g. if(IS_ENABLED(CONFIG_HVM)) { S; }
> + - Switch with a controlling value statically determined not to
> + match one or more case statements
I (continue to) consider this as too lax. I don't think we want to permit
something like
void test(uint8_t val)
{
switch ( val )
{
case 0x100:
...
Imo like in the earlier bullet point I think this wants limiting to
compile-time constant values, at least initially.
Jan
On Mon, 11 Sep 2023, Jan Beulich wrote:
> On 09.09.2023 01:03, Stefano Stabellini wrote:
> > From: Stefano Stabellini <stefano.stabellini@amd.com>
> >
> > During the discussions that led to the acceptance of Rule 2.1, we
> > decided on a few exceptions that were not properly recorded in
> > rules.rst. Add them now.
> >
> > Signed-off-by: Stefano Stabellini <stefano.stabellini@amd.com>
> > Acked-by: Jan Beulich <jbeulich@suse.com>
> > ---
> > Nicola, does this work with ECLAIR?
> >
> > I am referring to the locations of the SAF-2-safe tag on top of
> > call_psci_system_off, BUG, etc.
> >
> > Changes in v3:
> > - added SAF-2-safe to safe.json
> > - added a few SAF-2-safe examples
> > ---
> > docs/misra/rules.rst | 13 ++++++++++++-
> > docs/misra/safe.json | 8 ++++++++
> > xen/arch/arm/psci.c | 1 +
> > xen/arch/x86/shutdown.c | 1 +
> > xen/include/xen/bug.h | 2 ++
> > 5 files changed, 24 insertions(+), 1 deletion(-)
> >
> > diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> > index 34916e266a..82de4c645d 100644
> > --- a/docs/misra/rules.rst
> > +++ b/docs/misra/rules.rst
> > @@ -107,7 +107,18 @@ maintainers if you want to suggest a change.
> > * - `Rule 2.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_01_1.c>`_
> > - Required
> > - A project shall not contain unreachable code
> > - -
> > + - The following are allowed:
> > + - Invariantly constant conditions, e.g. if(IS_ENABLED(CONFIG_HVM)) { S; }
> > + - Switch with a controlling value statically determined not to
> > + match one or more case statements
>
> I (continue to) consider this as too lax. I don't think we want to permit
> something like
>
> void test(uint8_t val)
> {
> switch ( val )
> {
> case 0x100:
> ...
>
> Imo like in the earlier bullet point I think this wants limiting to
> compile-time constant values, at least initially.
Yes good point
© 2016 - 2024 Red Hat, Inc.