Re: ECLAIR Xen x86 results and progress

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

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.