Re: [XEN PATCH v3 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Julien Grall <julien@xxxxxxx>]

Hi,

On 08/11/2023 17:12, Nicola Vetrini wrote:
> On 2023-11-08 17:25, Julien Grall wrote:
> > Hi Stefano,
> >
> > On 07/11/2023 20:41, Stefano Stabellini wrote:
> > > +Julien, Andrew
> > >
> > > Julien and Andrew raised concerns on this patch on the Xen Matrix
> > > channel. Please provide further details.
> > Thanks! It looks like I was already CCed but this likely got lost with 
> > all the MISRA patches...
> > On Matrix, there was concerned raised that the documentation now have 
> > a dependency on C compiler and you are also build C files in docs.
> > In addition to that, I have a few more comments.
> The .rst file was chosen to have a human-readable format for the runtime 
> failures
> documentation. The other option that is otherwise viable is having a 
> dummy .c or .h in
> the sources (in this case it would likely be under xen/).
>
> The transformation of this file into a .c file could be done from xen's 
> Makefile of course,
> but I reckoned that would have been more difficult, as the Makefile for 
> the docs is
> far shorter
I understand that the Makefile for docs is shorter. However this seems 
to be the wrong place to "compile" a file.
I think it makes more sense to do it from xen/ as those deviations are 
only for the hypervisor. IOW they don't apply for the tools.
[....]

> > > > > +
> > > > > +all: $(TARGETS)
> > > > > +
> > > > > +# This Makefile will generate the object files indicated in 
> > > > > TARGETS by taking
> > > > > +# the corresponding .rst file, converting its content to a C block 
> > > > > comment and
> > > > > +# then compiling the resulting .c file. This is needed for the 
> > > > > file's content to
> > > > > +# be available when performing static analysis with ECLAIR on the 
> > > > > project.
> > I am a bit lost with the explanation. The generated object will be 
> > empty. So why do you require to generate it?
> See above. The only requirement is that some intercepted toolchain 
> invocation happens
> and that the processed file has a comment block containing the strings 
> specified below.
> The resulting artifact isn't needed in any way.
Just to confirm, there is no way for Eclair to specify some extra file 
that don't require "compilation"?
> > Furthermore, the content doesn't seem to follow a specific syntax (or 
> > at least it is not clear that it should follow one). So why do you 
> > need to expose the content to Eclair?
> Under the hood there's a regex matching the resulting comment block 
> against a set of default
> templates used to indicate that the project has some form of 
> documentation around runtime
> failures. The default templates are along these lines (the comment begin 
> and end markers
> need not be on the same line):
>
> /* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */
>
> If the string is matched, then documentation for that particular 
> category of runtime
> failures is deemed present, otherwise a violation will be reported (one 
> for each category).
> Both the categories and format of the string to be matched can be 
> customized, but I'd like
> to avoid doing that.
Ok. The format should be documented at top of the rst file so a 
developper knows how to modify the file correctly.
> > > > > +
> > > > > +# sed is used in place of cat to prevent occurrences of '*/'
> > > > > +# in the .rst from breaking the compilation
> > > > > +$(TARGETS:.o=.c): %.c: %.rst
> > > > > +    printf "/*\n\n" > $@.tmp
> > > > > +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
> > > > > +    printf "\n\n*/\n" >> $@.tmp
> > > > > +    mv $@.tmp $@
> > > > > +
> > > > > +%.o: %.c
> > > > > +    $(CC) -std=c99 -c $< -o $@
> > AFAICT, this will generate a file using the host compiler. This may be 
> > different from the compiler used to build Xen.
> > So I will repeat myself, how all of this matters? Maybe it would be 
> > useful if you provide some documentation from Eclair.
> > Cheers,
> The only non-trivial bit is that the file 
> automation/eclair_analysis/ECLAIR/toolchain.ecl
> specifies some compilers (if this needs to be adjusted to something 
> other that $(CC), then I
> may need some additional guidance) and the c99 standard, hence if you 
> use a different
> compiler ECLAIR will complain that you didn't document the toolchain 
> assumptions according
> to D1.1 (which is incidentally why we created the file 
> C-language-toolchain.rst).
We should use the same/compiler as used by the hypervisor. I feel 
anything else is just a gross hack and may break in the long term. Hence 
why it makes a lot more sense to generate/"compile" the file from the 
hypervisor Makefile.
Cheers,

--
Julien Grall