Re: ECLAIR Xen x86 results and progress

[Andrew Cooper <Andrew.Cooper3@xxxxxxxxxx>]

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