[XEN PATCH 0/3] Introduce and use static_assert_unreachable()

[XEN PATCH 0/3] Introduce and use static_assert_unreachable()

[Federico Serafini]

Introduce macro static_assert_unreachable(), use it to replace
__{get,put}_user_bad() and update ECLAIR configuration to allow the use of
such macro at the end of switch-caluses.

Federico Serafini (3):
  xen: introduce static_assert_unreachable()
  x86/uaccess: replace __{get,put}_user_bad() with
    static_assert_unreachable()
  automation/eclair: add deviation for MISRA C:2012 Rule 16.3

 automation/eclair_analysis/ECLAIR/deviations.ecl | 4 ++++
 docs/misra/deviations.rst                        | 4 ++++
 xen/arch/x86/include/asm/uaccess.h               | 7 ++-----
 xen/include/xen/compiler.h                       | 8 ++++++++
 4 files changed, 18 insertions(+), 5 deletions(-)

-- 
2.34.1

[XEN PATCH 1/3] xen: introduce static_assert_unreachable()

[Federico Serafini]

Introduce macro static_asser_unreachable() to check that a program
point is considered unreachable by the static analysis performed by the
compiler, even at optimization level -O0.

The use of such macro will lead to one of the following outcomes:
- the program point identified by the macro is considered unreachable,
  then the compiler removes the macro;
- the program point identified by the macro is not considered
  unreachable, then the compiler does not remove the macro, which will
  lead to a failure in the build process caused by an assembler error.

Signed-off-by: Federico Serafini <federico.serafini@bugseng.com>
---
 xen/include/xen/compiler.h | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/xen/include/xen/compiler.h b/xen/include/xen/compiler.h
index 16d554f2a5..ad0520f5d4 100644
--- a/xen/include/xen/compiler.h
+++ b/xen/include/xen/compiler.h
@@ -64,6 +64,14 @@
 # define fallthrough        do {} while (0)  /* fallthrough */
 #endif
 
+/*
+ * Add the following macro to check that a program point is considered
+ * unreachable by the static analysis performed by the compiler,
+ * even at optimization level -O0.
+ */
+#define static_assert_unreachable() \
+    asm(".error \"unreachable program point reached\"");
+
 #ifdef __clang__
 /* Clang can replace some vars with new automatic ones that go in .data;
  * mark all explicit-segment vars 'used' to prevent that. */
-- 
2.34.1

Re: [XEN PATCH 1/3] xen: introduce static_assert_unreachable()

[Jan Beulich]

On 22.01.2024 14:48, Federico Serafini wrote:
> Introduce macro static_asser_unreachable() to check that a program
> point is considered unreachable by the static analysis performed by the
> compiler, even at optimization level -O0.

Is it really intended to limit use of this macro to cases where even
at -O0 the compiler would eliminate respective code? Note that right
now even debug builds are done with some optimization, and some of
the DCE we're relying depends on that (iirc).

> --- a/xen/include/xen/compiler.h
> +++ b/xen/include/xen/compiler.h
> @@ -64,6 +64,14 @@
>  # define fallthrough        do {} while (0)  /* fallthrough */
>  #endif
>  
> +/*
> + * Add the following macro to check that a program point is considered
> + * unreachable by the static analysis performed by the compiler,
> + * even at optimization level -O0.
> + */
> +#define static_assert_unreachable() \
> +    asm(".error \"unreachable program point reached\"");

Did you check the diagnostic that results when this check actually
triggers? I expect it will be not really obvious from the message
you introduce where the issue actually is. I expect we will want
to use some of __FILE__ / __LINE__ / __FUNCTION__ to actually
supply such context.

Also: Stray semicolon and (nit) missing blanks.

Finally I wonder about case: We have ASSERT_UNREACHABLE() and it
may be indicated to use all uppercase her as well.

Jan

Re: [XEN PATCH 1/3] xen: introduce static_assert_unreachable()

[Federico Serafini]

On 22/01/24 15:02, Jan Beulich wrote:
> On 22.01.2024 14:48, Federico Serafini wrote:
>> Introduce macro static_asser_unreachable() to check that a program
>> point is considered unreachable by the static analysis performed by the
>> compiler, even at optimization level -O0.
> 
> Is it really intended to limit use of this macro to cases where even
> at -O0 the compiler would eliminate respective code? Note that right
> now even debug builds are done with some optimization, and some of
> the DCE we're relying depends on that (iirc).

I'll remove this restriction.


> 
>> --- a/xen/include/xen/compiler.h
>> +++ b/xen/include/xen/compiler.h
>> @@ -64,6 +64,14 @@
>>   # define fallthrough        do {} while (0)  /* fallthrough */
>>   #endif
>>   
>> +/*
>> + * Add the following macro to check that a program point is considered
>> + * unreachable by the static analysis performed by the compiler,
>> + * even at optimization level -O0.
>> + */
>> +#define static_assert_unreachable() \
>> +    asm(".error \"unreachable program point reached\"");
> 
> Did you check the diagnostic that results when this check actually
> triggers? I expect it will be not really obvious from the message
> you introduce where the issue actually is. I expect we will want
> to use some of __FILE__ / __LINE__ / __FUNCTION__ to actually
> supply such context.

The assembler error comes with file and line information, for example:

./arch/x86/include/asm/uaccess.h: Assembler messages:
./arch/x86/include/asm/uaccess.h:377: Error: unreachable program point 
reached

At line 377 there is an use of get_unsafe_size() where I passed a wrong
size as argument. Is that clear enough?

What do you think about modifying the message as follows:
"unreachability static assert failed."


> 
> Also: Stray semicolon and (nit) missing blanks.

It is not clear to me where are the missing blanks.


> 
> Finally I wonder about case: We have ASSERT_UNREACHABLE() and it
> may be indicated to use all uppercase her as well.

Ok.


-- 
Federico Serafini, M.Sc.

Software Engineer, BUGSENG (http://bugseng.com)

Re: [XEN PATCH 1/3] xen: introduce static_assert_unreachable()

[Jan Beulich]

On 24.01.2024 09:20, Federico Serafini wrote:
> On 22/01/24 15:02, Jan Beulich wrote:
>> On 22.01.2024 14:48, Federico Serafini wrote:
>>> --- a/xen/include/xen/compiler.h
>>> +++ b/xen/include/xen/compiler.h
>>> @@ -64,6 +64,14 @@
>>>   # define fallthrough        do {} while (0)  /* fallthrough */
>>>   #endif
>>>   
>>> +/*
>>> + * Add the following macro to check that a program point is considered
>>> + * unreachable by the static analysis performed by the compiler,
>>> + * even at optimization level -O0.
>>> + */
>>> +#define static_assert_unreachable() \
>>> +    asm(".error \"unreachable program point reached\"");
>>
>> Did you check the diagnostic that results when this check actually
>> triggers? I expect it will be not really obvious from the message
>> you introduce where the issue actually is. I expect we will want
>> to use some of __FILE__ / __LINE__ / __FUNCTION__ to actually
>> supply such context.
> 
> The assembler error comes with file and line information, for example:
> 
> ./arch/x86/include/asm/uaccess.h: Assembler messages:
> ./arch/x86/include/asm/uaccess.h:377: Error: unreachable program point 
> reached
> 
> At line 377 there is an use of get_unsafe_size() where I passed a wrong
> size as argument. Is that clear enough?

Hmm, yes, looks like it might be sufficient. Mentioning __FUNCTION__ may
still add value, though. But I see now that __FILE__ / __LINE__ are
already covered for.

> What do you think about modifying the message as follows:
> "unreachability static assert failed."

I'm okay-ish with the original text, and I like it slightly better than
this new suggestion. If we want "static assert" in the output, then maybe
"static assertion failed: unreachable".

>> Also: Stray semicolon and (nit) missing blanks.
> 
> It is not clear to me where are the missing blanks.

Just like for other keywords:

    asm ( ".error \"unreachable program point reached\"" )

Jan

[XEN PATCH 2/3] x86/uaccess: replace __{get,put}_user_bad() with static_assert_unreachable()

[Federico Serafini]

Use static_assert_unreachable() to improve readability and anticipate
the build failure (from a linker error to an assembler error) in case
of wrong size.

Signed-off-by: Federico Serafini <federico.serafini@bugseng.com>
---
 xen/arch/x86/include/asm/uaccess.h | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/xen/arch/x86/include/asm/uaccess.h b/xen/arch/x86/include/asm/uaccess.h
index 7443519d5b..ce608fc2b5 100644
--- a/xen/arch/x86/include/asm/uaccess.h
+++ b/xen/arch/x86/include/asm/uaccess.h
@@ -21,9 +21,6 @@ unsigned int copy_from_guest_ll(void *to, const void __user *from, unsigned int
 unsigned int copy_to_unsafe_ll(void *to, const void *from, unsigned int n);
 unsigned int copy_from_unsafe_ll(void *to, const void *from, unsigned int n);
 
-extern long __get_user_bad(void);
-extern void __put_user_bad(void);
-
 #define UA_KEEP(args...) args
 #define UA_DROP(args...)
 
@@ -208,7 +205,7 @@ do {                                                                       \
     case 8:                                                                \
         put_unsafe_asm(x, ptr, grd, retval, "q",  "", "ir", errret);       \
         break;                                                             \
-    default: __put_user_bad();                                             \
+    default: static_assert_unreachable();                                  \
     }                                                                      \
     clac();                                                                \
 } while ( false )
@@ -227,7 +224,7 @@ do {                                                                       \
     case 2: get_unsafe_asm(x, ptr, grd, retval, "w", "=r", errret); break; \
     case 4: get_unsafe_asm(x, ptr, grd, retval, "k", "=r", errret); break; \
     case 8: get_unsafe_asm(x, ptr, grd, retval,  "", "=r", errret); break; \
-    default: __get_user_bad();                                             \
+    default: static_assert_unreachable();                                  \
     }                                                                      \
     clac();                                                                \
 } while ( false )
-- 
2.34.1

[XEN PATCH 3/3] automation/eclair: add deviation for MISRA C:2012 Rule 16.3

[Federico Serafini]

Update ECLAIR configuration to consider safe switch clauses ending
with static_assert_unreachable().

Update docs/misra/deviations.rst accordingly.

Signed-off-by: Federico Serafini <federico.serafini@bugseng.com>
---
 automation/eclair_analysis/ECLAIR/deviations.ecl | 4 ++++
 docs/misra/deviations.rst                        | 4 ++++
 2 files changed, 8 insertions(+)

diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index fd32ff8a9c..b0cd904d2d 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -368,6 +368,10 @@ safe."
 -config=MC3R1.R16.3,reports+={safe, "any_area(end_loc(any_exp(text(/BUG\\(\\);/))))"}
 -doc_end
 
+-doc_begin="Switch clauses ending with failure method \"static_assert_unreachable()\" are safe."
+-config=MC3R1.R16.3,reports+={safe, "any_area(end_loc(any_exp(text(/static_assert_unreachable\\(\\);/))))"}
+-doc_end
+
 -doc_begin="Switch clauses not ending with the break statement are safe if an
 explicit comment indicating the fallthrough intention is present."
 -config=MC3R1.R16.3,reports+={safe, "any_area(end_loc(any_exp(text(^(?s).*/\\* [fF]all ?through.? \\*/.*$,0..1))))"}
diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
index 123c78e20a..875f0d9160 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -307,6 +307,10 @@ Deviations related to MISRA C:2012 Rules:
      - Switch clauses ending with failure method \"BUG()\" are safe.
      - Tagged as `safe` for ECLAIR.
 
+   * - R16.3
+     - Switch clauses ending with macro static_assert_unreachable() are safe.
+     - Tagged as `safe` for ECLAIR.
+
    * - R16.3
      - Existing switch clauses not ending with the break statement are safe if
        an explicit comment indicating the fallthrough intention is present.
-- 
2.34.1