ECLAIR Xen x86 results and progress

ECLAIR Xen x86 results and progress

[Stefano Stabellini]

Hi all,

Roberto kindly provided the ECLAIR x86 results:

https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/

Click on "See ECLAIR in action", then you can select "Show 100 entries"
and see all the results in one page. As an example MC3R1.R1.3
corresponds to Rule 1.3 in the spreadsheet.


If you are OK with this, I would like to aim at a follow-up meeting on
Tue May 17 at the same time (8AM California / 4PM UK). If the date/time
doesn't work, I'll run another Doodle poll.

By then, I am hoping that the group has already gone through the first
20 rules in the list, up until Rule 8.10. Is that reasonable for all of
you?

Cheers,

Stefano

Re: ECLAIR Xen x86 results and progress

[Andrew Cooper]

On 06/05/2022 17:31, Stefano Stabellini wrote:
> Hi all,
>
> Roberto kindly provided the ECLAIR x86 results:
>
> https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/
>
> Click on "See ECLAIR in action", then you can select "Show 100 entries"
> and see all the results in one page. As an example MC3R1.R1.3
> corresponds to Rule 1.3 in the spreadsheet.

Thanks.  Some observations:

1) D4.10 "use header guards to prevent multiple inclusion"

asm/p2m.h lacks header guards at all.  asm/softirq.h has some decidedly
dodgy looking logic.  These should obviously be fixed, and there are
probably more too in the 57 violations.

However, we have files like public/errno.h which are explicitly designed
to be included multiple times, and are not going to change unless we
have a fundamental shift in opinion on the utility of trying to make a
single set of header files for all environments.

Also, Eclair really doesn't like how we include C files.  TBH, I don't
much either, but some of the hypercall compat logic explicitly depends
on including itself, to avoid coding the hypercall logic twice.  There
is an argument to say that this is differently-less-bad than other
options, but it certainly doesn't help with general comprehensibility of
the code.

2) R6.2 "don't use signed bitfields"

We have one single violation, and it's only used as a regular boolean. 
It doesn't even need to be a bitfield at all, because there's 63 bits of
padding at the end of sh_emulate_ctxt.

(In the time that I've been browsing, someone has apparently done
another build with in particular CONFIG_SHADOW_PAGING disabled, so this
has fallen off the list of violations.)

3) R8.10 "inline functions shall be static".

We have 3 violations.  One is a legitimate complaint in spinlock.c.

The other two violations are from extern inline.  Given that extern
inline explicitly gives the compiler the choice to inline, or use a
single common out-of-line implementation, I think extern inline also
meets the spirit of what MISRA is trying to do here, insofar as it
prevents there being dead functions emitted into the final binary.

~Andrew

Re: ECLAIR Xen x86 results and progress

[Stefano Stabellini]

[-- Attachment #1: Type: text/plain, Size: 3251 bytes --]

On Fri, 6 May 2022, Andrew Cooper wrote:
> On 06/05/2022 17:31, Stefano Stabellini wrote:
> > Hi all,
> >
> > Roberto kindly provided the ECLAIR x86 results:
> >
> > https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/
> >
> > Click on "See ECLAIR in action", then you can select "Show 100 entries"
> > and see all the results in one page. As an example MC3R1.R1.3
> > corresponds to Rule 1.3 in the spreadsheet.
> 
> Thanks.  Some observations:
> 
> 1) D4.10 "use header guards to prevent multiple inclusion"
> 
> asm/p2m.h lacks header guards at all.  asm/softirq.h has some decidedly
> dodgy looking logic.  These should obviously be fixed, and there are
> probably more too in the 57 violations.
> 
> However, we have files like public/errno.h which are explicitly designed
> to be included multiple times, and are not going to change unless we
> have a fundamental shift in opinion on the utility of trying to make a
> single set of header files for all environments.
> 
> Also, Eclair really doesn't like how we include C files.  TBH, I don't
> much either, but some of the hypercall compat logic explicitly depends
> on including itself, to avoid coding the hypercall logic twice.  There
> is an argument to say that this is differently-less-bad than other
> options, but it certainly doesn't help with general comprehensibility of
> the code.

I think we should accept this rule because in general we would want new
headers to follow the rule. We should fix things like asm/p2m.h, and we
should deviate (not fix, but document) any of the existing cases we
don't want to fix (e.g. errno.h.)


> 2) R6.2 "don't use signed bitfields"
> 
> We have one single violation, and it's only used as a regular boolean. 
> It doesn't even need to be a bitfield at all, because there's 63 bits of
> padding at the end of sh_emulate_ctxt.

This is an easy rule to follow


> (In the time that I've been browsing, someone has apparently done
> another build with in particular CONFIG_SHADOW_PAGING disabled, so this
> has fallen off the list of violations.)
>
> 3) R8.10 "inline functions shall be static".
> 
> We have 3 violations.  One is a legitimate complaint in spinlock.c.
> 
> The other two violations are from extern inline.  Given that extern
> inline explicitly gives the compiler the choice to inline, or use a
> single common out-of-line implementation, I think extern inline also
> meets the spirit of what MISRA is trying to do here, insofar as it
> prevents there being dead functions emitted into the final binary.

As we only have 3 violations, it is another easy rule to follow.

The reason for the rule seems to be to avoid undefined behavior which
can happen if the inline function (not static) is defined with external
linkage but it is not defined in the same translation unit. Looking at
the code, we are using extern gnu_inline which actually has a defined
behavior, so it looks like we are meeting the spirit of the MISRA rule.

In any case, the details on those 2 violations don't matter too much. I
think we should accept the rule because if someone submitted a patch
with an inline function (non static) we would definitely ask them why,
and we would want ECLAIR to highlight the issue.

Re: ECLAIR Xen x86 results and progress

[Bertrand Marquis]

Hi Stefano,

> On 6 May 2022, at 17:31, Stefano Stabellini <sstabellini@kernel.org> wrote:
> 
> Hi all,
> 
> Roberto kindly provided the ECLAIR x86 results:
> 
> https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/
> 
> Click on "See ECLAIR in action", then you can select "Show 100 entries"
> and see all the results in one page. As an example MC3R1.R1.3
> corresponds to Rule 1.3 in the spreadsheet.
> 
> 
> If you are OK with this, I would like to aim at a follow-up meeting on
> Tue May 17 at the same time (8AM California / 4PM UK). If the date/time
> doesn't work, I'll run another Doodle poll.

Works for me.
> 
> By then, I am hoping that the group has already gone through the first
> 20 rules in the list, up until Rule 8.10. Is that reasonable for all of
> you?

I completed that part of the table this morning (up to 8.14), it took me 30 minutes.

Cheers
Bertrand

> 
> Cheers,
> 
> Stefano

Re: ECLAIR Xen x86 results and progress

[Stefano Stabellini]

On Mon, 9 May 2022, Bertrand Marquis wrote:
> > On 6 May 2022, at 17:31, Stefano Stabellini <sstabellini@kernel.org> wrote:
> > 
> > Hi all,
> > 
> > Roberto kindly provided the ECLAIR x86 results:
> > 
> > https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/
> > 
> > Click on "See ECLAIR in action", then you can select "Show 100 entries"
> > and see all the results in one page. As an example MC3R1.R1.3
> > corresponds to Rule 1.3 in the spreadsheet.
> > 
> > 
> > If you are OK with this, I would like to aim at a follow-up meeting on
> > Tue May 17 at the same time (8AM California / 4PM UK). If the date/time
> > doesn't work, I'll run another Doodle poll.
> 
> Works for me.

Actually, to make sure more people are able to attend, I would like to
suggest May 19 8AM California / 4PM UK / 5PM Europe (which is the same
slot typically used by the Xen Community Call). Please let me know if
that works or if it is a problem.


> > By then, I am hoping that the group has already gone through the first
> > 20 rules in the list, up until Rule 8.10. Is that reasonable for all of
> > you?
> 
> I completed that part of the table this morning (up to 8.14), it took me 30 minutes.

Thank you! I did so as well in about the same amount of time.

I think I should provide a clarification on a couple of rules that are
not clear from the examples.


# Rule 5.4 "Macro identifiers shall be distinct"

This one is about the length of the Macro itself. C90 requires the first
31 characters to be different, while C99 requires the first 63
characteres to be different.

So the problem is the following:

#define this_macro_is_way_way_way_too_long
#define this_macro_is_way_way_way_too_loooong

I don't think we have any violations.


# Rule 8.6 " An identifier with external linkage shall have exactly one external definition"

This one is meant to catch cases where there are 2 definitions for 1
declaration:

header.h:
extern int hello;

file1.c:
int hello;

file2:
int hello;

There was a question on whether having 1 declaration with no definitions
would be OK, so only the following:

header.h:
extern int hello;

for instance because file1.c has been removed from the build due to a
kconfig. Reading MISRA, I don't think it is a violation of Rule 8.6.
Roberto please correct me if I am wrong.


Cheers,

Stefano

Re: ECLAIR Xen x86 results and progress

[Stefano Stabellini]

On Mon, 9 May 2022, Stefano Stabellini wrote:
> On Mon, 9 May 2022, Bertrand Marquis wrote:
> > > On 6 May 2022, at 17:31, Stefano Stabellini <sstabellini@kernel.org> wrote:
> > > 
> > > Hi all,
> > > 
> > > Roberto kindly provided the ECLAIR x86 results:
> > > 
> > > https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/
> > > 
> > > Click on "See ECLAIR in action", then you can select "Show 100 entries"
> > > and see all the results in one page. As an example MC3R1.R1.3
> > > corresponds to Rule 1.3 in the spreadsheet.
> > > 
> > > 
> > > If you are OK with this, I would like to aim at a follow-up meeting on
> > > Tue May 17 at the same time (8AM California / 4PM UK). If the date/time
> > > doesn't work, I'll run another Doodle poll.
> > 
> > Works for me.
> 
> Actually, to make sure more people are able to attend, I would like to
> suggest May 19 8AM California / 4PM UK / 5PM Europe (which is the same
> slot typically used by the Xen Community Call). Please let me know if
> that works or if it is a problem.

Quick update: we are making excellent progress with the spreadsheet, 4
out of 6 people have already completed scoring the first set of 20
rules.

I'll send a calendar invite for May 19 8AM California as it looks like
we'll be able to make it.

Re: ECLAIR Xen x86 results and progress

[Roberto Bagnara]

On 09/05/22 21:55, Stefano Stabellini wrote:
> On Mon, 9 May 2022, Bertrand Marquis wrote:
>>> On 6 May 2022, at 17:31, Stefano Stabellini <sstabellini@kernel.org> wrote:
>>>
>>> Hi all,
>>>
>>> Roberto kindly provided the ECLAIR x86 results:
>>>
>>> https://eclairit.com:8443/job/XEN/Target=X86_64,agent=public/lastSuccessfulBuild/eclair/
>>>
>>> Click on "See ECLAIR in action", then you can select "Show 100 entries"
>>> and see all the results in one page. As an example MC3R1.R1.3
>>> corresponds to Rule 1.3 in the spreadsheet.
>>>
>>>
>>> If you are OK with this, I would like to aim at a follow-up meeting on
>>> Tue May 17 at the same time (8AM California / 4PM UK). If the date/time
>>> doesn't work, I'll run another Doodle poll.
>>
>> Works for me.
> 
> Actually, to make sure more people are able to attend, I would like to
> suggest May 19 8AM California / 4PM UK / 5PM Europe (which is the same
> slot typically used by the Xen Community Call). Please let me know if
> that works or if it is a problem.
> 
> 
>>> By then, I am hoping that the group has already gone through the first
>>> 20 rules in the list, up until Rule 8.10. Is that reasonable for all of
>>> you?
>>
>> I completed that part of the table this morning (up to 8.14), it took me 30 minutes.
> 
> Thank you! I did so as well in about the same amount of time.
> 
> I think I should provide a clarification on a couple of rules that are
> not clear from the examples.
> 
> 
> # Rule 5.4 "Macro identifiers shall be distinct"
> 
> This one is about the length of the Macro itself. C90 requires the first
> 31 characters to be different, while C99 requires the first 63
> characteres to be different.
> 
> So the problem is the following:
> 
> #define this_macro_is_way_way_way_too_long
> #define this_macro_is_way_way_way_too_loooong
> 
> I don't think we have any violations.
> 
> 
> # Rule 8.6 " An identifier with external linkage shall have exactly one external definition"
> 
> This one is meant to catch cases where there are 2 definitions for 1
> declaration:
> 
> header.h:
> extern int hello;
> 
> file1.c:
> int hello;
> 
> file2:
> int hello;
> 
> There was a question on whether having 1 declaration with no definitions
> would be OK, so only the following:
> 
> header.h:
> extern int hello;
> 
> for instance because file1.c has been removed from the build due to a
> kconfig. Reading MISRA, I don't think it is a violation of Rule 8.6.
> Roberto please correct me if I am wrong.

Hi there.

As I am not 100% sure I will be able to attend the meeting on the 19th,
I am providing some input here:

# Rule 5.4 "Macro identifiers shall be distinct"

The point here is that every standard-conformant C/C++ compiler has the right
of ignoring the characters in an identifier that are outside the "significant
part."  Different kind of identifiers have different minimum lengths
for the significant part.  For macros and non-external identifiers,
we have:

- for C90 and C95: 31 characters;
- for C99, C11 and C18: 63 characters;
- for C++: 1024 characters.

So, for example, a C90 compiler (or, and it is the same, any compiler
in C90 mode) can freely ignore all characters in the name of macros
beyond the 31st.  And if two macro identifiers differ only in the
non-significant part, the behavior is undefined (for the simple reason
that the preprocessor can choose any of the conflicting macros).
Now, the builds of XEN that are analized at https://eclairit.com
are built with (versions of) GCC and GCC goes well beyond the
standard minimal requirements by stipulating that "For internal names,
all characters are significant. For external names, the number of
significant characters are defined by the linker; for almost all
targets, all characters are significant."
(https://gcc.gnu.org/onlinedocs/gcc/Identifiers-implementation.html#Identifiers-implementation).
Now, given that ECLAIR takes into account (completely automatically)
all the implementation-defined behaviors of the actually used toolchain
(including how those are influenced by the command-line options),
why do we have a violation report when macro names only differ
after the 31st character in C90 mode?
For example,

12345678901234567890123456789012345678901
XEN_NETIF_CTRL_TYPE_SET_HASH_MAPPING_SIZE
XEN_NETIF_CTRL_TYPE_SET_HASH_MAPPING

?

The reason is pragmatic: yes, there is no undefined behavior
with GCC, but do you really want to admit macro names that are
different only in characters coming hundreds or thousands positions
from the beginning of the identifier?  I guess not: then choose your
threshold, add a one-liner to the ECLAIR configuration, and let ECLAIR
warn you if and when the rule is violated with *that* threshold.

This brings us to a related topic: why is part of XEN compiled in C90
mode while part of it is compiled in C99 mode?  This is a very important
violation of MISRA C Rule 1.1, which is not in your coding standard,
but it really should be included.  C90 and C99 are not 100% compatible,
and mixing them is asking for trouble.  My advice is choosing one version
of the language (C90, C99, C11 or C18) and stick to it, enabling Rule 1.1
to make sure the source code complies to the chosen language standard version.
My advice is: if at all possible, exclude C90;  then use the most modern
version of the language that is compatible with *all* toolchains you need
to support.

# Rule 8.6 " An identifier with external linkage shall have exactly one external definition"

Exactly one means:

- 2 or more is bad, as you may violate the "one definition rule" and incur
   undefined behavior;
- 0 is bad, as this means you have redundant (useless) declarations.

Of course, the first case is the most dangerous one.  The second case
is just one aspect of a more general MISRA principle saying
"unused stuff should not reach the compilation phases past preprocessing,"
that is, you should #if-, #ifdef- or #ifndef-out everything that is
not required by the project configuration you are building.
Again, the actual hazard depends on several factors.  Unused function
definitions are clearly more dangerous than unused function declarations:
if the linker is unable to filter out the unused code, then the device
will contain code that is unreachable in normal executions but that
code can be exploited during a cyber-attack.  It is a matter of a one-line
ECLAIR configuration to adapt to the case where you might say
"unused declarations are OK and we do not want to exclude them
with preprocessor conditionals."

I hope it helps,

     Roberto

Re: ECLAIR Xen x86 results and progress

[Jan Beulich]

On 09.05.2022 21:55, Stefano Stabellini wrote:
> # Rule 8.6 " An identifier with external linkage shall have exactly one external definition"
> 
> This one is meant to catch cases where there are 2 definitions for 1
> declaration:
> 
> header.h:
> extern int hello;
> 
> file1.c:
> int hello;
> 
> file2:
> int hello;

Which won't build (link) anyway with our use of -fno-common.

Jan